Haskell：在类型系统中指定列表的等长约束 [英] Haskell: Specifying equal-length constraints of lists in the type system
问题描述
f 这样的函数，它接受一个列表并返回一个等长的列表： f :: [a] - > [a] - 长度f（xs）==长度xs
同样，我可能有一个函数例如 g ，它接受两个长度相等的列表：
g :: [a] - > [a] - > ...
如果 f 和 g 按上述类型输入，那么如果不满足与长度相关的约束，则可能导致运行时错误。因此，我想在类型系统中编码这些约束。我该怎么做？
请注意，我正在寻找一种可用于日常情况的实用框架，为代码添加尽可能少的直观开销。我特别感兴趣的是你自己如何处理 f 和 g ;也就是说，你会试图将长度相关的约束添加到它们的类型中，就像这里提到的那样，或者为了代码的简单性而将它们留在上面给出的类型中？
以下代码由 Gabriel Gonzalez的博客结合评论中提供的一些信息：
{ - ＃LANGUAGE GADTs，DataKinds＃ - }
数据Nat = Z | S Nat
- 类型'a'的长度为'n'的持有值列表
数据列表na其中
无::列表Z a
缺点： ：a - >列表m a - >列表（S m）a
- 仅用于可视化（更好的实例可以读取）
实例显示a => Show（List na）where
show Nil =Nil
show（Cons x xs）= show x ++ - ++ show xs
g ::（a →b→c）→>列表n a - >列表n b - >清单nc
gf（Cons x xs）（Cons y ys）= Cons（fxy）$ gf xs ys
gf无无=无
l1 =缺点1（缺点2（无））:: List（S（SZ））Int
l2 = Cons 3（Cons 4（Nil））:: List（S（SZ））Int
l3 =缺点5（无）:: List（SZ）Int
main :: IO（）
main = print $ g（+）l1 l2
- 这会导致GHC抛出一个错误：
- print $ g
$ b 这个替代列表定义（使用GADT和DataKinds）对其类型中的列表的长度进行编码。如果你然后定义你的函数 g :: List n a - >列表n a - > ... 如果列表长度不一样，类型系统会报错。
如果这可能（可以理解）太多对你来说是额外的复杂情况，我不确定使用类型系统是否可行。最简单的方法是使用monad / applicative（例如 Maybe 或> ）定义 g code>），让 g 根据两个输入将元素添加到列表中，并对结果进行排序。 I.e。
g ::（a - > b - > c） - > [a] - > [b] - >可能[c]
gf l1 l2 = sequence $ g'f l1 l2
其中g'f（x：xs）（y：ys）=（Just $ fxy）：g'f xs ys
$ main $（）
main = do print $ g（
$ b $） +）[1,2] [2,3,4] - Nothing
print $ g（+）[1,2,3] [2,3,4] - Just [3,5,7 ]
In Haskell, I often have a function like f, which accepts a list and returns a list of equal length:
f :: [a] -> [a] -- length f(xs) == length xs
Similarly, I might have a function like g, which accepts two lists that should be of equal length:
g :: [a] -> [a] -> ...
If f and g are typed as above, then run-time errors may result if their length-related constraints are not satisfied. I would therefore like to encode these constraints in the type system. How might I do this?
Please note that I'm looking for a practical framework that may be used in everyday situations, adding as little intuitive overhead to the code as possible. I am particularly interested to know how you would deal with f and g yourself; that is, would you attempt to add the length-related constraints to their types, as asked here, or would you leave them with the types as given above for simplicity of code?
解决方案 The following code is adapted from Gabriel Gonzalez's blog in combination with some information supplied in the comments:
{-# 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
This alternative list definition (using GADTs and DataKinds) encodes the length of a list in its type. If you then define your function g :: List n a -> List n a -> ... the type system will complain if the lists are not of the same length.
In case this would (understandably) be too much extra complication for you, I'm not sure using the type system would be the way to go. The easiest is to define g using a monad/applicative (e.g. Maybe or Either), let g add elements to your list depending on both inputs, and sequence the result. I.e.
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：在类型系统中指定列表的等长约束的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
