Sono possibili prove di istanze familiari di tipo?

Question

Per prima cosa, ho iniziato con alcuni tipi di numeri naturali tipici di tipo livello.

{-# 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) 

Quindi volevo creare un tipo di dati che rappresentasse una griglia n-dimensionale. (Una generalizzazione di ciò che si trova al 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 

L'idea è che il tipo U num x è il tipo di un num griglia dimensionale di x s, che è "concentrato" su un punto della griglia .

così ho voluto rendere questo un comonad, e ho notato che c'è questa funzione potenzialmente utile che posso fare:

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) 

possiamo ora implementare una "dimensione join" che trasforma una griglia n-dimensionale griglie m-dimensionali in una griglia dimensionale (n + m), in termini di questo combinatore. Questo sarà utile quando si ha a che fare con il risultato di cojoin che produrrà griglie di griglie.

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

Fin qui tutto bene. Ho anche notato che l'istanza Functor può essere scritta in termini di ufold.

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

Tuttavia, ciò provoca un errore di tipo.

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

Ma se improvvisare qualche pasta copia, quindi l'errore di tipo va via.

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) 

Beh, odio il sapore della pasta, quindi la mia domanda è questa. Come posso dire al sistema di tipi che Plus n Z è uguale a n? E il problema è questo: non è possibile modificare le istanze di tipo family che potrebbero causare dimJoin per produrre un errore di tipo simile.

Answer 1

Quello che vi serve è un bel tipo di uguaglianza proposizionale: si

{-# 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 

Questo permette di provare cose arbitrarie sui tuoi tipi e portare quella conoscenza in ambito locale dal pattern matching sul Refl.

Una cosa fastidiosa è che la mia prova plusZero richiede l'induzione sulla natura in questione, che non sarà possibile eseguire in base all'impostazione predefinita (poiché non esiste in fase di esecuzione). Una classe di caratteri per generare testimoni Natural sarebbe facile, però.

Un'altra opzione per il caso specifico potrebbe essere solo quella di invertire gli argomenti su più nella definizione del tipo in modo da ottenere il Z sulla sinistra e si riduce automaticamente. Spesso è un buon primo passo per assicurarsi che i tuoi tipi siano semplici come puoi crearli, ma poi avrai spesso bisogno dell'uguaglianza proposizionale per cose più complicate, a prescindere.