Инвертирование семейства типов

У меня есть семейство "линейного" типа, т.е. вида

type family Foo a
type instance Foo T1 = T2
type instance Foo T2 = T3
...
type instance Foo T9 = T10

В моем частном случае использования очень удобно определить "обратное" семейство FooRev, а затем применить ограничение (FooRev (Foo x) ~ x):

type family FooRev a
type instance FooRev T10 = T9
type instance FooRev T9 = T8
...
type instance FooRev T2 = T1

Обратное семейство позволяет GHC выводить множество типов, которые в противном случае были бы неоднозначными из-за неинъективности. По сути, это та же идея, что была предложена здесь. Это решение работает довольно хорошо, но необходимость определять «обратное» семейство типов, перечисляя все случаи, раздражает, программно и подвержено ошибкам. Есть ли более общий способ определить обратную сторону линейного семейства, например Foo?


haskell type-families
person crockeea    schedule 24.10.2014    source источник
comment
Возможно, вы могли бы как-то использовать data семейства, которые известны как инъективные. Не уверен, подходит ли это к вашей проблеме.   -  person luqui    schedule 24.10.2014
comment
Метапрограммирование (например, Template Haskell) может генерировать и то, и другое, сохраняя ваш код СУХИМ, если это вас беспокоит. В противном случае вы могли бы определить список ассоциаций уровня типа, поиск уровня типа, уровень типа map swap и получить оба семейства типов из списка.   -  person chi    schedule 24.10.2014
comment
@luqui Я только что видел это перед публикацией, но насколько я знаю, это не совсем то, что мне нужно. В моем случае все Ti относятся к типу Bar a b c, параметры которого меняются. Это не вписывается в семейство данных, не так ли?   -  person crockeea    schedule 24.10.2014
comment
@chi Может быть, вы могли бы продемонстрировать одну из этих идей?   -  person crockeea    schedule 24.10.2014

Ответы (2)


arrow_upward
5
arrow_downward

Я думаю, что FunctionalDependencies должно быть лучшим решением для вашего случая:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}

class Foo a b | a -> b, b -> a
instance Foo T1 T2
instance Foo T2 T3
...

Теперь каждый b может быть выведен из a и наоборот.

person András Kovács    schedule 24.10.2014

arrow_upward
5
arrow_downward

Я решил попробовать идею @ chi, но в конце концов придумал что-то попроще.

{-# LANGUAGE TypeOperators, DataKinds, TypeFamilies #-}

type family NextElt (a :: *) (xs :: [*]) where
  NextElt a (a ': b ': cs) = b
  NextElt a (b ': c ': cs) = NextElt a (c ': cs)

type family PrevElt (a :: *) (xs :: [*]) :: * where
  PrevElt a (b ': a ': xs) = b
  PrevElt a (b ': c ': xs) = PrevElt a (c ': xs)

data T1
data T2
data T3
type TSeq = '[T1, T2, T3]

type NextRp a = NextElt a TSeq
type PrevRp a = PrevElt a TSeq

Использование списка типов для представления линейной последовательности типов позволяет мне выразить отношения, не записывая каждый тип дважды (что необходимо при использовании экземпляров семейства типов или экземпляров класса). В перечисленных выше типах семейств используется метод скользящего окна для поиска элемента в списке с предыдущим или следующим элементом. Эти семейства типов являются общими (и могут быть расширены для работы с типами, отличными от *, используя Data.Type.Equality.)

person crockeea    schedule 24.10.2014