Czy są możliwe testy typu rodzinnego?

Question

Najpierw zacząłem od typowych rzeczy o typie naturalnym.

{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE GADTs #-} 
{-# LANGUAGE TypeFamilies #-} 

data Nat = Z | S Nat 

type family Plus (n :: Nat) (m :: Nat) :: Nat 
type instance Plus Z m = m 
type instance Plus (S n) m = S (Plus n m) 

Tak więc chciałem stworzyć typ danych reprezentujący n-wymiarową siatkę. (A uogólnienie tego, co znajduje się na Evaluating cellular automata is comonadic.)

data U (n :: Nat) x where 
    Point  :: x       -> U Z  x 
    Dimension :: [U n x] -> U n x -> [U n x] -> U (S n) x 

Chodzi o to, że typ U num x jest typ num wymiarowej siatki x S, który jest „skoncentrowany” na określonym punkcie w siatce .

Chciałem więc zrobić to comonad, i zauważyłem, że jest to potencjalnie użyteczna funkcja mogę zrobić:

ufold :: (x -> U m r) -> U n x -> U (Plus n m) r 
ufold f (Point x) = f x 
ufold f (Dimension ls mid rs) = 
    Dimension (map (ufold f) ls) (ufold f mid) (map (ufold f) rs) 

Możemy teraz zaimplementować „wymiar join”, który włącza n-wymiarowej siatki m-wymiarowe siatki w (n + m) -wymiarowej siatce, w kategoriach tego kombinatora. Przyda się to, gdy mamy do czynienia z wynikiem cojoin, który będzie wytwarzał siatki z siatek.

dimJoin :: U n (U m x) -> U (Plus n m) x 
dimJoin = ufold id 

Jak dotąd tak dobrze. Zauważyłem również, że instancja Functor może być napisana pod kątem ufold.

instance Functor (U n) where 
    fmap f = ufold (\x -> Point (f x)) 

Jednak powoduje to błąd typu.

Couldn't match type `n' with `Plus n 'Z' 

Ale jeśli wymiemy trochę makaronu do kopiowania, błąd typu zniknie.

instance Functor (U n) where 
    fmap f (Point x) = Point (f x) 
    fmap f (Dimension ls mid rs) = 
    Dimension (map (fmap f) ls) (fmap f mid) (map (fmap f) rs) 

Dobrze nienawidzę smak kopiowania makaron, więc moje pytanie jest takie. Jak mogę powiedzieć systemowi typu, że Plus n Z jest równy n? A pułapka jest taka: nie można dokonać zmian w instancjach rodziny typów, które spowodowałyby błąd typu podobnego do dimJoin.

Answer 1

Co trzeba to ładne propositional typu równość:

{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE PolyKinds #-} 
{-# LANGUAGE GADTs #-} 
{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE TypeOperators #-} 

data Nat = Z | S Nat 

type family Plus (n :: Nat) (m :: Nat) :: Nat 
type instance Plus Z m = m 
type instance Plus (S n) m = S (Plus n m) 

data (:=) :: k -> k -> * where 
    Refl :: a := a 

data Natural (n :: Nat) where 
    Zero :: Natural Z 
    Suc :: Natural n -> Natural (S n) 

plusZero :: Natural n -> n := (n `Plus` Z) 
plusZero Zero = Refl 
plusZero (Suc n) | Refl <- plusZero n = Refl 

Pozwala to na dowolne rzeczy okazać się o swoich typów i doprowadzić tę wiedzę do zakresu lokalnie przez wzór pasujący na Refl.

Jedną denerwującą rzeczą jest to, że mój dowód plusZero wymaga indukcji ponad rzeczową, której nie można wykonać domyślnie (ponieważ nie istnieje w środowisku wykonawczym). Jednak typeklass do generowania świadków byłby łatwy.

Inną opcją dla konkretnego przypadku może być po prostu odwrócenie argumentów na plus w definicji typu, aby uzyskać po lewej stronie wartość Z, która zmniejsza się automagicznie. Często jest to dobry pierwszy krok, aby upewnić się, że twoje typy są tak proste, jak tylko możesz je zrobić, ale wtedy często będziesz potrzebować równoznacznej propozycji dla bardziej skomplikowanych rzeczy, niezależnie.