Можно ли определить типы данных с переменным числом родов? - PullRequest
Новая
       40

Можно ли определить типы данных с переменным числом родов?

0 голосов
/ 11 сентября 2018

Я могу определить поликлиническое естественное преобразование следующим образом: 

type family (~>) :: k -> k -> *
type instance (~>) = (->)

newtype NT a b = NT { apply :: forall x. a x ~> b x }
type instance (~>) = NT

, которое работает во всех видах, поэтому я могу определить, например, 

left :: Either ~> (,)
left = NT (NT (Left . fst))

Это круто и вдохновляет.Но независимо от того, сколько трюков я играю, я не могу получить что-то вариативное в типе return .Например, я хотел бы 

type family (:*:) :: k -> k -> k
type instance (:*:) = (,)
type instance (:*:) = ???

Кажется, что это невозможно, поскольку семейства типов должны быть полностью насыщенными, и вы можете вводить конструкторы типов только в *.

Я даже попробовал несколько довольно неприятных трюков 

type instance (:*:) = Promote2 (:*:)

type family Promote2 :: (j -> k -> l) -> (a -> j) -> (a -> k) -> (a -> l) where

promote2_law :: Promote2 f x y z :~: f (x z) (y z)
promote2_law = unsafeCoerce Refl

fstP :: forall (a :: k -> *) (b :: k -> *) (c :: k). (a :*: b) c -> a c
fstP = case promote2_law @(:~:) @a @b @c of Refl -> NT (\(a,b) -> a)

И я не знаю, есть ли у этого хоть какая-то надежда на работу, так как я не думал о том, как более добрые вещи«представлены».Но GHC знает, что я все равно лгу 

• Couldn't match type ‘(,)’ with ‘Promote2 (,) a’
  Inaccessible code in
    a pattern with constructor: Refl :: forall k (a :: k). a :~: a,

Есть ли другие способы для этого?

1 Ответ

0 голосов
/ 11 сентября 2018

«Аксиоматический» подход действительно работает, я только что использовал неправильное равенство: 

fstP :: forall (a :: j -> k) (b :: j -> k) (x :: j). (a :*: b) x -> a x
fstP = castWith (Refl ~% promote2_law @(:*:) @a @b @x ~% Refl) fst
    where
    infixl 9 ~%
    (~%) = Data.Type.Equality.apply

Использование Equality.apply важно для информирования средства проверки типов о том, где применять аксиому.Я сделал полную разработку продуктов более высокого класса для справки.

Будьте осторожны, когда я играл с этим, я однажды испытал панику GHC.Так что неприятные трюки могут быть неприятными.Все еще интересуются другими подходами.

...