Deklarowanie wystąpień sparametryzowanych typów synonimów

Question

Mam wiele funkcji, które działają na wektory, tj. Listy z wymuszonymi typami długościami.

Próbuję aby moje typy łatwiej napisać, to znaczy zamiast pisać

foo :: (Fold Integer v, Map Integer Integer v v, ...) => ... 

mam uznającą nową klasę NList więc mogę tylko napisać foo :: NList v Integer => ...

The (uproszczony) klasy wygląda następująco:

class (Fold (v i) i 
     , Map i i (v i) (v i) 
     , Map i (Maybe i) (v i) (v (Maybe i)) 
    ) => NList v i 

jak widać, mam zachować „wektor” typ odrębny od „pozycji” typu (tzn v oddzielny od i), aby móc wykonywać operacje takie jak Map na wektorach Maybe.

Jako takie, v musi mieć rodzaj * -> * i i rodzaj *.

Jednak gdy próbuję instancję wektorami tak:

instance NList Vec2 Integer 
instance NList Vec3 Integer 
... 

pojawia się następujący błąd:

Type synonym `Vec2' should have 1 argument, but has been given none 
In the instance declaration for `NList Vec2 Integer' 

Teraz jestem bardzo nowy typ poziomie programowania, i rozumiem, że prawdopodobnie robię to w bardzo zacofany sposób. Czy możliwe jest utworzenie takiego synonimu typu? Czy każdy typ-czarodziej ma sugestie dotyczące lepszych sposobów na osiągnięcie moich celów?

Answer 1

Problem polega na tym, że Vec2 i Vec3 są przypuszczalnie zadeklarowane jako coś takiego:

type Vec2 a = Vec (S (S Z)) a 
type Vec3 a = Vec (S (S (S Z))) a 

Synonimy typu nie mogą być częściowo stosowana, z różnych powodów magicznych (będą one prowadzić do lambda typu poziomu, który spustoszenie wraków z wszelkiego rodzaju rzeczami związanymi z rozwiązywaniem i wnioskami instancji - wyobraź sobie, że możesz zdefiniować type Id a = a i uczynić z niego instancję Monad).

To znaczy, nie można dokonać Vec2 instancję niczego, ponieważ nie można używać Vec2 jakby to był rodzaj konstruktor pełni fledge z rodzaju * -> *; to efektywne "makro" typu, które można w pełni zastosować.

Jednak może określić typ jako synonimy cząstkowych wniosków siebie:

type Vec2 = Vec (S (S Z)) 
type Vec3 = Vec (S (S (S Z))) 

te są równoważne z tym, że instancje będą dozwolone.

Jeśli typ Vec3 faktycznie wygląda

type Vec3 a = Cons a (Cons a (Cons a Nil))) 

lub podobne, to masz pecha; będziesz musiał użyć wrappera newtype, jeśli chcesz podać dowolne wystąpienia.(Z drugiej strony, powinieneś być w stanie uniknąć definiowania instancji bezpośrednio na tych typach całkowicie dając instancje dla Nil i Cons zamiast, co pozwala na użycie Vec3 jako przykład).

Należy zauważyć, że z nowego GHC 7.4 constraint kinds, można uniknąć całkowicie odrębny typ, a po prostu zdefiniować synonim wiązania:

type NList v i = 
    (Fold (v i) i 
    , Map i i (v i) (v i) 
    , Map i (Maybe i) (v i) (v (Maybe i)) 
    ) 

Jeśli chodzi o swoim podejściu w ogóle idzie, powinien w zasadzie działać poprawnie; ten sam ogólny pomysł jest używany przez pakiet . Ogromna liczba klas i dużych kontekstów może sprawić, że komunikaty o błędach będą bardzo mylące i spowolnią kompilację, ale taka jest natura hackery typu na poziomie. Jednakże, jeśli masz podstawową Vec typ zdefiniowany jako zwykłej GADT:

data Vec n a where 
    Nil :: Vec Z a 
    Succ :: a -> Vec n a -> Vec (S n) a 

wtedy rzeczywiście nie potrzebuje żadnych typeclasses w ogóle. Jeśli jest to zdefiniowane w inny sposób, ale nadal jest sparametryzowana na typ poziomie naturalnym, można wymienić wszystkie klasy z jednym:

data Proxy s = Proxy 

class Nat n where 
    natElim 
     :: ((n ~ Z) => r) 
     -> (forall m. (n ~ S m, Nat m) => Proxy m -> r) 
     -> Proxy n 
     -> r 

To powinno pozwolić na wyeliminowanie konteksty zupełnie, ale sprawia, że ​​definiowanie operacji na wektorach nieco trudniejsze.