Binding Name in Typ Unterschrift mit DataKind

Question

So fand ich endlich eine Aufgabe, wo ich die neue Erweiterung DataKinds (mit ghc 7.4.1) verwenden könnte. Hier ist die Vec Ich verwende:

data Nat = Z | S Nat deriving (Eq, Show) 

data Vec :: Nat -> * -> * where 
    Nil :: Vec Z a 
    Cons :: a -> Vec n a -> Vec (S n) a 

nun der Einfachheit halber wollte ich fromList implementieren. Grundsätzlich kein Problem mit einfacher Rekursion/Faltung - aber ich kann mir nicht vorstellen, wie man den richtigen Typ gibt. Als Referenz ist dies die Agda Version:

fromList : ∀ {a} {A : Set a} → (xs : List A) → Vec A (List.length xs) 

Mein Haskell Ansatz, mit der Syntax I here sah:

fromList :: (ls :: [a]) -> Vec (length ls) a 
fromList [] = Nil 
fromList (x:xs) = Cons x (fromList xs) 

Das gibt mir ein parse error on input 'a'. Ist die Syntax, die ich gefunden habe, sogar korrekt, oder haben sie sie geändert? Ich fügte auch einige Erweiterungen hinzu, die im Code in der Verbindung sind, die auch nicht half (zZ habe ich GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, UndecidableInstances).

Mein anderer Verdacht war, dass ich einfach nicht polymorphe Typen binden, aber mein Test dafür:

bla :: (n :: Nat) -> a -> Vec (S n) a 
bla = undefined 

scheiterte auch mit Kind mis-match Expected kind 'ArgKind', but 'n' has kind 'Nat' (nicht wirklich wissen, was das bedeutet).

Könnte mir jemand mit einer funktionierenden Version von fromList helfen und auch die anderen Probleme klären? Leider ist DataKinds noch nicht sehr gut dokumentiert und scheint davon auszugehen, dass jeder, der es benutzt, profunde Kenntnisse der Typentheorie besitzt.

Answer 1

Haskell, im Gegensatz zu Agda, hat keine abhängigen Typen, also gibt es keine Möglichkeit genau das zu tun, was Sie wollen. Typen können nicht nach Wert parametrisiert werden, da Haskell eine Phasendifferenz zwischen Laufzeit und Kompilierzeit erzwingt. Die Art und Weise, wie DataKinds konzeptionell funktioniert, ist eigentlich sehr einfach: Datentypen sind gefördert zu Arten (Typen von Typen) und Datenkonstruktoren werden zu Typen heraufgestuft.

fromList :: (ls :: [a]) -> Vec (length ls) a 

hat ein paar Probleme: (ls :: [a]) nicht wirklich Sinn machen (zumindest, wenn Sie nur vorgetäuscht abhängige Typen mit Förderung) und length ist eine Variable vom Typ anstelle eine Typ-Funktion. Was Sie sagen wollen, ist

fromList :: [a] -> Vec ??? a 

wo ??? die Länge der Liste ist. Das Problem ist, dass Sie bei der Kompilierung keine Art, die Länge der Liste haben ... so könnten wir

fromList :: [a] -> Vec len a 

versuchen, aber das ist falsch, weil es sagt, dass fromList eine Liste von beliebiger Länge zurückkehren kann. Stattdessen, was wir sagen möchten, ist

fromList :: exists len. [a] -> Vec len a 

aber Haskell unterstützt dies nicht. Statt

data VecAnyLength a where 
    VecAnyLength :: Vec len a -> VecAnyLength a 

cons a (VecAnyLength v) = VecAnyLength (Cons a v) 

fromList :: [a] -> VecAnyLength a 
fromList []  = VecAnyLength Nil 
fromList (x:xs) = cons x (fromList xs) 

Sie können tatsächlich ein VecAnyLength durch Musterabgleich verwenden und somit einen immer (lokal) psuedo abhängig typisierten Wert.ähnlich

,

bla :: (n :: Nat) -> a -> Vec (S n) a 

funktioniert nicht, weil Haskell Funktionen nur Argumente der Art * nehmen. Stattdessen könnten Sie versuchen

data HNat :: Nat -> * where 
    Zero :: HNat Z 
    Succ :: HNat n -> HNat (S n) 

bla :: HNat n -> a -> Ven (S n) a 

die selbst definierbar ist

bla Zero a  = Cons a Nil 
bla (Succ n) a = Cons a (bla n a) 

Answer 2

Sie hier einige typeclass Magie verwenden können (siehe HList für weitere Informationen):

{-# LANGUAGE GADTs, KindSignatures, DataKinds, FlexibleInstances 
    , NoMonomorphismRestriction, FlexibleContexts #-} 

data Nat = Z | S Nat deriving (Eq, Show) 

data Vec :: Nat -> * -> * where 
    Nil :: Vec Z a 
    Cons :: a -> Vec n a -> Vec (S n) a 

instance Show (Vec Z a) where 
    show Nil = "." 

instance (Show a, Show (Vec m a)) => Show (Vec (S m) a) where 
    show (Cons x xs) = show x ++ " " ++ show xs 

class FromList m where 
    fromList :: [a] -> Vec m a 

instance FromList Z where 
    fromList [] = Nil 

instance FromList n => FromList (S n) where 
    fromList (x:xs) = Cons x $ fromList xs 

t5 = fromList [1, 2, 3, 4, 5] 

aber das ist nicht wirklich das Problem lösen :

> :t t5 
t5 :: (Num a, FromList m) => Vec m a 

Listen werden zur Laufzeit gebildet wird, deren Länge nicht zum Zeitpunkt der Kompilierung bekannt ist, so dass der Compiler den Typ für t5 nicht ableiten kann, muss sie explizit angegeben werden:

*Main> t5 

<interactive>:99:1: 
    Ambiguous type variable `m0' in the constraint: 
     (FromList m0) arising from a use of `t5' 
    Probable fix: add a type signature that fixes these type variable(s) 
    In the expression: t5 
    In an equation for `it': it = t5 
*Main> t5 :: Vec 'Z Int 
*** Exception: /tmp/d.hs:20:3-19: Non-exhaustive patterns in function fromList 

*Main> t5 :: Vec ('S ('S ('S 'Z))) Int 
1 2 3 *** Exception: /tmp/d.hs:20:3-19: Non-exhaustive patterns in function fromList 

*Main> t5 :: Vec ('S ('S ('S ('S ('S 'Z))))) Int 
1 2 3 4 5 . 
*Main> t5 :: Vec ('S ('S ('S ('S ('S ('S ('S 'Z))))))) Int 
1 2 3 4 5 *** Exception: /tmp/d.hs:23:3-40: Non-exhaustive patterns in function fromList 

Sprachen mit abhängigen Arten haben Karten von Begriffe zu Typen, Typen können auch zur Laufzeit dynamisch gebildet werden, so dass dieses Problem nicht existiert.