Jak stworzyć "klasę rodzajową" w Haskell lub polimorfizm ad-hoc na poziomie typu za pomocą rodzin typu

Question

Studiuję cechy rodziny typów Haskella i obliczenia typu. Wydaje się to dość łatwo dostać się polimorfizm parametryczny na poziomie typu używając PolyKinds:

{-# LANGUAGE DataKinds, TypeFamilies, KindSignatures, GADTs, TypeOperators, UndecidableInstances, PolyKinds, MultiParamTypeClasses, FlexibleInstances #-} 

data NatK = Z | S NatK 
data IntK = I NatK NatK 

infix 6 + 
type family (x :: NatK) + (y :: NatK) :: NatK where 
    Z  + y = y 
    (S x) + y = S (x + y) 

-- here's a parametrically polymorphic (==) at the type-level 
-- it also deals specifically with the I type of kind IntK 
infix 4 == 
type family (a :: k) == (b :: k) :: Bool where 
    (I a1 a2) == (I b1 b2) = (a1 + b2) == (a2 + b1) 
    a == a = True 
    a == b = False 

mogę robić takie rzeczy jak :kind! Bool == Bool lub :kind! Int == Int lub :kind! Z == Z i :kind! (I Z (S Z)) == (I (S Z) (S (S Z))).

Jednak chcę utworzyć polimorficzny ad-hoc type +. Tak więc jest ograniczony do instancji, które mu podaję. 2 wystąpienia tutaj byłyby rodzajami NatK i rodzajami IntK.

raz pierwszy spróbował co parametrycznie polimorficzny:

infix 6 :+ 
type family (x :: k) :+ (y :: k) :: k where 
    Z   :+ y = y 
    (S x)  :+ y = S (x :+ y) 
    (I x1 x2) :+ (I y1 y2) = I (x1 :+ y1) (x2 :+ y2) 

To działa, jak mogę zrobić :kind! (I (S Z) Z) :+ (I (S Z) Z).

Mogę również wykonać: :kind! Bool :+ Bool. I to nie ma sensu, ale pozwala na to jako prosty konstruktor typów. Chcę utworzyć rodzinę typów, która nie pozwala na takie błędne typy.

W tym momencie jestem zagubiony. Próbowałem klasy typów z parametrem type. Ale to nie zadziałało.

class NumK (a :: k) (b :: k) where 
    type Add a b :: k 

instance NumK (Z :: NatK) (b :: NatK) where 
    type Add Z b = b 

instance NumK (S a :: NatK) (b :: NatK) where 
    type Add (S a) b = S (Add a b) 

instance NumK (I a1 a2 :: IntK) (I b1 b2 :: IntK) where 
    type Add (I a1 a2) (I b1 b2) = I (Add a1 b1) (Add a2 b2) 

Nadal zezwala na :kind! Add Bool Bool.

Czy to ma coś wspólnego z rozszerzeniem ConstraintKinds, gdy trzeba ograniczyć :+ lub Add do pewnego rodzaju „klasy”?

Answer 1

Najprostszym rozwiązaniem jest użycie otwartych rodzin typu dla przeciążenia ad-hoc i zamkniętych rodzin typu realizacji:

data NatK = Z | S NatK 
data IntK = I NatK NatK 

type family Add (x :: k) (y :: k) :: k 

type family AddNatK (a :: NatK) (b :: NatK) where 
    AddNatK Z b = b 
    AddNatK (S a) b = S (AddNatK a b) 

type family AddIntK (a :: IntK) (b :: IntK) where 
    AddIntK (I a b) (I a' b') = I (AddNatK a a') (AddNatK b b') 

type instance Add (a :: NatK) (b :: NatK) = AddNatK a b 
type instance Add (a :: IntK) (b :: IntK) = AddIntK a b 

Jeśli chcemy wiele metod typu i poziomu określenie poziomu zgrupowane razem, możemy napisać miłe zajęcia korzystając z użyciem KProxyData.Proxy:

class NumKind (kproxy :: KProxy k) where 
    type Add (a :: k) (b :: k) :: k 
    -- possibly other methods on type or term level 

instance NumKind ('KProxy :: KProxy NatK) where 
    type Add a b = AddNatK a b 

instance NumKind ('KProxy :: KProxy IntK) where 
    type Add a b = AddIntK a b 

oczywiście związane typy są takie same jak otwartego typu Familie s, więc mogliśmy również użyć rodzin typu otwartego z oddzielną klasą dla metod na poziomie terminala. Ale myślę, że generalnie czystsze jest posiadanie wszystkich przeciążonych nazwisk w tej samej klasie.

Od GHC 8.0 KProxy staje się zbędne, ponieważ rodzaje i typy będą traktowane w ten sam sposób:

{-# LANGUAGE TypeInType #-} 

import Data.Kind (Type) 

class NumKind (k :: Type) where 
    type Add (a :: k) (b :: k) :: k 

instance NumKind NatK where 
    type Add a b = AddNatK a b 

instance NumKind IntK where 
    type Add a b = AddIntK a b 

Answer 2

(Powinno to być komentarz, ale potrzebuję więcej miejsca)

Próbowałem coś jak

class GoodK (Proxy k) => NumK (a :: k) (b :: k) where ... 

ale nie udało mi się. Nie mam pojęcia, czy to, o co prosisz, jest osiągalne.

Najlepszym przybliżeniem, jakie otrzymałem, jest sprawdzenie rodzaju, ale wygenerowanie nierozwiązywalnego ograniczenia, więc jeśli kiedykolwiek go użyjemy, i tak otrzymamy błąd. Być może to może wystarczyć dla twoich celów (?).

class Fail a where 

instance Fail a => NumK (a :: *) (b :: *) where 
    type Add a b =()