{-# LANGUAGE DataKinds,GADTs,KindSignatures #-}
-- a kind declaration
data Nat = Z | S Nat
data SafeList :: (Nat -> * -> *) where
Nil :: SafeList Z a
Cons :: a -> SafeList n a -> SafeList (S n) a
-- the type signature ensures that the input list has at least one element
safeHead :: SafeList (S n) a -> a
safeHead (Cons x xs) = x
这似乎工作：
ghci> :t Cons 5 (Cons 3 Nil)
Cons 5 (Cons 3 Nil) :: Num a => SafeList ('S ('S 'Z)) a
ghci> safeHead (Cons 'x' (Cons 'c' Nil))
'x'
ghci> safeHead Nil
Couldn't match type 'Z with 'S n0
Expected type: SafeList ('S n0) a0
Actual type: SafeList 'Z a0
In the first argument of `safeHead',namely `Nil'
In the expression: safeHead Nil
In an equation for `it': it = safeHead Nil
然而,为了使这个数据类型真正有用,我应该可以从编译时不知道长度的运行时数据构建它.我天真的尝试：
fromList :: [a] -> SafeList n a fromList = foldr Cons Nil
这无法编译,类型错误：
Couldn't match type 'Z with 'S n
Expected type: a -> SafeList n a -> SafeList n a
Actual type: a -> SafeList n a -> SafeList ('S n) a
In the first argument of `foldr',namely `Cons'
In the expression: foldr Cons Nil
In an equation for `fromList': fromList = foldr Cons Nil
我明白为什么会发生这种情况：对于每次迭代迭代,缺点的返回类型是不同的 – 这就是整体而言！但是我看不清楚,可能是因为我没有深入阅读这个主题. (我不能想象所有这些努力都被放在一个不可能在实践中使用的类型系统中！)
那么,如何从“普通”简单类型的数据构建这种依赖类型的数据？
以下@ luqui的建议我能够使fromList编译：
data ASafeList a where
ASafeList :: SafeList n a -> ASafeList a
fromList :: [a] -> ASafeList a
fromList = foldr f (ASafeList Nil)
where f x (ASafeList xs) = ASafeList (Cons x xs)
这是我尝试解压缩ASafeList并使用它：
getSafeHead :: [a] -> a getSafeHead xs = case fromList xs of ASafeList ys -> safeHead ys
这会导致另一种类型错误：
Couldn't match type `n' with 'S n0
`n' is a rigid type variable bound by
a pattern with constructor
ASafeList :: forall a (n :: Nat). SafeList n a -> ASafeList a,in a case alternative
at SafeList.hs:33:22
Expected type: SafeList ('S n0) a
Actual type: SafeList n a
In the first argument of `safeHead',namely `ys'
In the expression: safeHead ys
In a case alternative: ASafeList ys -> safeHead ys
再次,直观地说,这是无法编译的.我可以用一个空列表调用fromList,所以编译器不能保证我能够在安全列表上调用safeHead.这种缺乏知识大概是存在的ASafeList捕获.
这个问题可以解决吗？我觉得我可能已经走下了一个逻辑的死胡同.
如果你要麻烦一个列表来制作一个长度索引的列表(在文献中被称为“矢量”),你可以记住它的长度.
所以,我们有
data Nat = Z | S Nat data Vec :: Nat -> * -> * where -- old habits die hard VNil :: Vec Z a VCons :: a -> Vec n a -> Vec (S n) a
但是我们也可以给出静态长度的运行时间表示.理查德·艾森伯格(Richard Eisenberg)的“单身人士”包将为您做到这一点,但基本思想是为静态数字提供一种运行时间表示.
data Natty :: Nat -> * where Zy :: Natty Z Sy :: Natty n -> Natty (S n)
至关重要的是,如果我们有一个类型为Natty n的值,那么我们可以询问该值以找出什么是n.
Hasochists知道运行时间的代表性往往很无聊,即使一台机器也可以管理它,所以我们把它隐藏在类型类中
class NATTY (n :: Nat) where natty :: Natty n instance NATTY Z where natty = Zy instance NATTY n => NATTY (S n) where natty = Sy natty
现在我们可以从您的列表中获得一些稍长一点的内容,对您的长度进行详细的描述.
data LenList :: * -> * where LenList :: NATTY n => Vec n a -> LenList a lenList :: [a] -> LenList a lenList [] = LenList VNil lenList (x : xs) = case lenList xs of LenList ys -> LenList (VCons x ys)
您可以获得与长度破坏版本相同的代码,但是您可以随时随地获取长度的运行时间表示,并且您不需要沿向量爬行即可获取它.
当然,如果你希望长度是一个纳特,那还是一个痛苦,你反而有一个Natty n为一些n.
杂乱无章是个错误.
首先,让我为LenList添加一个解包器,它给你手中的数字.
unLenList :: LenList a -> (forall n. Natty n -> Vec n a -> t) -> t unLenList (LenList xs) k = k natty xs
现在我想定义
vhead :: Vec (S n) a -> a vhead (VCons a _) = a
执行安全财产.如果我有一个运行时间表示矢量的长度,我可以看看它是否vhead适用.
headOrBust :: LenList a -> Maybe a headOrBust lla = unLenList lla $\ n xs -> case n of Zy -> Nothing Sy _ -> Just (vhead xs)
所以你看一件事,在这样做的时候,了解另一件事.
