sir*_*ton 9 haskell type-systems list dependent-type
在Haskell中,我经常有一个函数f,它接受一个列表并返回一个相等长度的列表:
f :: [a] -> [a] -- length f(xs) == length xs
同样,我可能有一个函数g,它接受两个长度相等的列表:
g :: [a] -> [a] -> ...
如果f和g上面键入,则如果不满足与长度相关的约束,则可能导致运行时错误.因此,我想在类型系统中编码这些约束.我怎么能这样做？
请注意,我正在寻找可在日常情况下使用的实用框架,尽可能减少对代码的直观开销.我特别想知道你将如何f与g自己打交道; 也就是说,您是否会尝试将与长度相关的约束添加到其类型中,如此处所述,或者为了简化代码,您是否会使用上面给出的类型？
以下代码改编自Gabriel Gonzalez的博客,并结合评论中提供的一些信息:
{-# LANGUAGE GADTs, DataKinds #-}
data Nat = Z | S Nat
-- A List of length 'n' holding values of type 'a'
data List n a where
Nil :: List Z a
Cons :: a -> List m a -> List (S m) a
-- Just for visualization (a better instance would work with read)
instance Show a => Show (List n a) where
show Nil = "Nil"
show (Cons x xs) = show x ++ "-" ++ show xs
g :: (a -> b -> c) -> List n a -> List n b -> List n c
g f (Cons x xs) (Cons y ys) = Cons (f x y) $ g f xs ys
g f Nil Nil = Nil
l1 = Cons 1 ( Cons 2 ( Nil ) ) :: List (S (S Z)) Int
l2 = Cons 3 ( Cons 4 ( Nil ) ) :: List (S (S Z)) Int
l3 = Cons 5 (Nil) :: List (S Z) Int
main :: IO ()
main = print $ g (+) l1 l2
-- This causes GHC to throw an error:
-- print $ g (+) l1 l3
此备用列表定义(使用GADT和DataKinds)对其类型中的列表长度进行编码.如果然后定义了函数,g :: List n a -> List n a -> ...则类型系统会在列表长度不同时发出抱怨.
万一这会(理解上)对你来说太复杂了,我不确定使用类型系统是否可行.最简单的方法是g使用monad/applicative(例如Maybe或者Either)进行定义,让我们g根据两个输入向列表中添加元素,并对结果进行排序.即
g :: (a -> b -> c) -> [a] -> [b] -> Maybe [c]
g f l1 l2 = sequence $ g' f l1 l2
where g' f (x:xs) (y:ys) = (Just $ f x y) : g' f xs ys
g' f [] [] = []
g' f _ _ = [Nothing]
main :: IO ()
main = do print $ g (+) [1,2] [2,3,4] -- Nothing
print $ g (+) [1,2,3] [2,3,4] -- Just [3,5,7]
您观察到的缺点是因为长度信息不是列表类型的一部分; 因为类型检查器用于推理类型,所以除非不变量属于参数本身的类型,或者类型类约束或类型基于族的等式,否则不能在函数中指定不变量.(有一些haskell预处理器,比如Liquid Haskell,它允许你用这样的不变量来注释函数,这些函数将在编译时检查.)
有许多haskell库提供类似列表的数据结构,其长度在类型中编码.一些值得注意的是线性(带V)和固定向量.
这样的界面V是这样的:
f :: V n a -> V n a -> V n a
g :: V n a -> V n a -> [a]
-- or --
g :: V n a -> V n a -> V ?? a -- if ?? can be determined at compile-time
请注意我们的第一个类型签名的特定模式g:我们在两个类型中关注长度,并返回一个不关心长度,丢失信息的类型.
在第二种情况下,如果我们做对结果的长度照顾,长度在编译时间,这是有意义的是已知的.
请注意,V从线性实际上不包装列表,而是从矢量库中包含Vector.它还需要镜头(即线性库),如果你想要的只是长度编码的矢量,这无疑是一个很大的依赖.我认为固定向量的向量类型确实使用的东西更像是普通的haskell列表......但我并不完全确定.在任何情况下,它都有一个Foldable实例,因此您可以将其转换为列表.
当然要记住,如果你计划在这样的函数中编码长度...... Haskell/GHC必须能够看到你的实现类型检查!对于大多数这些库,Haskell将能够检测这样的事情(如果你坚持像压缩和fmapping,绑定,ap-ping这样的东西).对于大多数有用的情况,这是真的......但是,有时你的实现不能被编译器"证明",所以你必须在脑海中"证明"它,并使用某种不安全的强制.