Istanze e vincoli definiti in modo ricorsivo

Question

Ho giocato con vettori e matrici in cui la dimensione è codificata nel loro tipo, utilizzando la nuova estensione DataKinds. Si va sostanzialmente in questo modo:

data Nat = Zero | Succ Nat 

data Vector :: Nat -> * -> * where 
    VNil :: Vector Zero a 
    VCons :: a -> Vector n a -> Vector (Succ n) a 

Ora vogliamo casi tipici come Functor e Applicative. Functor è facile:

instance Functor (Vector n) where 
    fmap f VNil = VNil 
    fmap f (VCons a v) = VCons (f a) (fmap f v) 

Ma con l'istanza Applicative c'è un problema: Non sappiamo che tipo di tornare in puro. Possiamo comunque definire l'istanza induttivamente sulla dimensione del vettore:

instance Applicative (Vector Zero) where 
    pure = const VNil 
    VNil <*> VNil = VNil 

instance Applicative (Vector n) => Applicative (Vector (Succ n)) where 
    pure a = VCons a (pure a) 
    VCons f fv <*> VCons a v = VCons (f a) (fv <*> v) 

Tuttavia, anche se questo caso vale per tutti i vettori, il tipo di controllo non lo sa, quindi dobbiamo trasportare il vincolo Applicative ogni volta che usiamo l'istanza.

Ora, se questo si applica solo all'istanza Applicative, non sarebbe un problema, ma si scopre che il trucco delle dichiarazioni di istanze ricorsive è essenziale quando si programma con tipi come questi. Ad esempio, se si definisce una matrice come un vettore di vettori riga utilizzando la libreria TypeCompose,

type Matrix nx ny a = (Vector nx :. Vector ny) a 

dobbiamo definire una classe di tipo e aggiungere dichiarazioni istanza ricorsive di attuare sia la trasposizione e moltiplicazione matriciale. Questo porta a un'enorme proliferazione di vincoli che dobbiamo portare in giro ogni volta che usiamo il codice, anche se le istanze si applicano effettivamente a tutti i vettori e matrici (rendendo il tipo di vincoli inutile).

C'è un modo per evitare di dover aggirare tutti questi limiti? Sarebbe possibile estendere il controllo di tipo in modo che possa rilevare tali costruzioni induttive?

Answer 1

La definizione di pure è davvero al centro del problema. Quale dovrebbe essere il suo tipo, pienamente quantificato e qualificato?

pure :: forall (n :: Nat) (x :: *). x -> Vector n x   -- (X) 

non va bene, come non ci sono informazioni disponibili in fase di esecuzione per determinare se pure dovrebbe emettere VNil o VCons. Corrispondentemente, allo stato attuale, non si può semplicemente avere

instance Applicative (Vector n)        -- (X) 

Cosa si può fare? Beh, lavorare con il Strathclyde Haskell Enhancement, nel file Vec.lhs esempio, definisco un precursore di pure

vec :: forall x. pi (n :: Nat). x -> Vector {n} x 
vec {Zero} x = VNil 
vec {Succ n} x = VCons x (vec n x) 

con un tipo pi, che richiede che una copia di n essere passato in fase di esecuzione. Questo pi (n :: Nat). desugars come

forall n. Natty n -> 

dove Natty, con un nome più prosaico nella vita reale, è il Singleton GADT date da

data Natty n where 
    Zeroy :: Natty Zero 
    Succy :: Natty n -> Natty (Succ n) 

e le parentesi graffe nelle equazioni per vec solo si traducono Nat costruttori per Natty costruttori.Definisco quindi la seguente istanza diabolica (disattivando l'istanza di Functor predefinita)

instance {:n :: Nat:} => Applicative (Vec {n}) where 
    hiding instance Functor 
    pure = vec {:n :: Nat:} where 
    (<*>) = vapp where 
    vapp :: Vec {m} (s -> t) -> Vec {m} s -> Vec {m} t 
    vapp VNil   VNil   = VNil 
    vapp (VCons f fs) (VCons s ss) = VCons (f s) vapp fs ss 

che richiede ulteriore tecnologia, ancora. Il vincolo {:n :: Nat:} desugars a qualcosa che richiede che esista un testimone Natty n, e dalla potenza delle variabili di tipo scoped, le stesse citazioni {:n :: Nat:} che testimoniano esplicitamente. Longhand, che è

class HasNatty n where 
    natty :: Natty n 
instance HasNatty Zero where 
    natty = Zeroy 
instance HasNatty n => HasNatty (Succ n) where 
    natty = Succy natty 

e sostituire il vincolo {:n :: Nat:} con HasNatty n ed il corrispondente termine con (natty :: Natty n). Fare questa costruzione equivale sistematicamente a scrivere un frammento di un typececker Haskell nella classe di tipo Prolog, che non è la mia idea di gioia, quindi uso un computer.

Si noti che l'istanza Traversable (Perdonate la mia parentesi idioma e la mia silenziosa predefinita Functor e le istanze pieghevoli) non richiede jiggery quali pokery

instance Traversable (Vector n) where 
    traverse f VNil   = (|VNil|) 
    traverse f (VCons x xs) = (|VCons (f x) (traverse f xs)|) 

Questo è tutto la struttura è necessario per ottenere la moltiplicazione di matrici senza ricorsione ulteriori esplicito.

TL; DR Utilizzare la costruzione singleton e la classe del tipo associata per comprimere tutte le istanze ricorsivamente definite nell'esistenza di un runtime di test per i dati a livello di carattere, da cui è possibile eseguire il calcolo mediante ricorsione esplicita.

Quali sono le implicazioni del design?

GHC 7.4 ha la tecnologia di promozione del tipo, ma SHE ha ancora la costruzione singleton pi tipi da offrire. Una cosa chiaramente importante sui tipi di dati promossi è che sono chiusi, ma questo non è ancora mostrato in modo pulito: la costruibilità dei testimoni singleton è la manifestazione di quella chiusura. In qualche modo, se hai forall (n :: Nat). allora è sempre ragionevole richiedere anche un singleton, ma fare così fa la differenza con il codice generato: se è esplicito come nel mio costrutto pi, o implicito come nel dizionario per {:n :: Nat:}, c'è un extra informazioni di runtime da imbragare, e un teorema libero corrispondentemente più debole.

Una domanda di progettazione aperta per le versioni future di GHC è come gestire questa distinzione tra la presenza e l'assenza di testimoni di runtime ai dati a livello di codice. Da un lato, ne abbiamo bisogno in termini di vincoli. D'altra parte, abbiamo bisogno di pattern-match su di loro. Per esempio, dovrebbe significare la pi (n :: Nat). esplicito

forall (n :: Nat). Natty n -> 

o implicita

forall (n :: Nat). {:n :: Nat:} => 

? Naturalmente, lingue come Agda e Coq hanno entrambe le forme, quindi forse Haskell dovrebbe seguire l'esempio. C'è sicuramente spazio per fare progressi e ci stiamo lavorando!