Nombre de enlace en tipo de firma usando DataKind

Question

Por lo tanto, finalmente encontré una tarea donde podría hacer uso de la nueva extensión DataKinds (usando ghc 7.4.1). Aquí está el Vec que estoy usando:

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 

Ahora, por conveniencia que quería poner en práctica fromList. Básicamente no hay problema con la recursión/plegado simple, pero no puedo encontrar la forma de darle el tipo correcto. A modo de referencia, esta es la versión Agda:

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

enfoque Mi Haskell, usando la sintaxis vi here:

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

Esto me da una parse error on input 'a'. ¿La sintaxis que encontré es incluso correcta, o la han cambiado? También agregué algunas extensiones más que están en el código en el enlace, que tampoco ayudó (actualmente tengo GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, UndecidableInstances).

Mi otra sospecha era que yo no puedo obligar tipos polimórficos, pero mi prueba para esto:

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

fallado, también, con Kind mis-match Expected kind 'ArgKind', but 'n' has kind 'Nat' (no se sabe muy bien lo que significa).

¿Alguien me podría ayudar con una versión de trabajo de fromList y también aclarar los otros problemas? Desafortunadamente, DataKinds aún no está bien documentado y parece suponer que todos los que lo utilizan tienen un profundo conocimiento de la teoría de tipos.

Answer 1

Haskell, a diferencia de Agda, no tiene tipos dependientes, por lo que no hay forma de hacer exactamente lo que quiere. Los tipos no se pueden parametrizar por valor, ya que Haskell impone una distinción de fase entre el tiempo de ejecución y el tiempo de compilación. La forma en que DataKinds funciona conceptualmente es en realidad muy simple: los tipos de datos son promovidos a tipos (tipos de tipos) y los constructores de datos se promueven a tipos.

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

tiene un par de problemas: (ls :: [a]) no tiene mucho sentido (al menos cuando sólo está imitando tipos dependientes de la promoción), y length es una variable de tipo en lugar de una función de tipo. Lo que se quiere decir es

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

donde ??? es la longitud de la lista. El problema es que no hay manera de conseguir la longitud de la lista en tiempo de compilación ... así que podría intentar

fromList :: [a] -> Vec len a 

pero esto es incorrecto, ya que dice que fromList puede devolver una lista de cualquier longitud. En cambio, lo que queremos decir es

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

pero Haskell no es compatible con esto. En lugar

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) 

en realidad se puede utilizar un VecAnyLength por coincidencia de patrones, y conseguir así un valor (localmente) pseudo-dependiente mecanografiado.

Del mismo modo,

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

no funciona porque las funciones Haskell sólo pueden tomar argumentos de tipo *. En su lugar puede intentar

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

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

que es aún definible

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

Answer 2

Se puede utilizar un poco de magia clase de tipos aquí (ver HList para más):

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

pero esto no realmente resolver el problema :

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

listas se forman en tiempo de ejecución, su longitud no se conoce en tiempo de compilación, por lo que el compilador no puede deducir el tipo de t5, se debe especificar explícitamente:

*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 

Idiomas con tipos dependientes tienen mapas de términos a tipos, los tipos también se pueden formar dinámicamente en tiempo de ejecución, por lo que este problema no existe.