如何表达'takeWhile for vectors'的类型？
How can I express the type of 'takeWhile for vectors'?
Haskell 初学者。我定义了以下类型：
data Nat = Z | S Nat
data Vector a n where
Nil :: Vector a Z
(:-) :: a -> Vector a n -> Vector a (S n)
infixl 5 :-
我正在尝试编写函数 takeWhileVector，其行为与 takeWhile 在列表上的行为相同，但在向量上。
我的实现如下：
takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m
takeWhileVector f Nil = Nil
takeWhileVector f (x :- xs) = if (f x) then (x :- takeWhileVector f xs) else Nil
这不会编译并产生以下错误：
Could not deduce (m ~ 'S n0)
from the context (n ~ 'S n1)
bound by a pattern with constructor
:- :: forall a (n :: Nat). a -> Vector a n -> Vector a ('S n),
in an equation for ‘takeWhileVector’
at takeWhileVector.hs:69:20-26
‘m’ is a rigid type variable bound by
the type signature for
takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m
at takeWhileVector.hs:67:20
Expected type: Vector a m
Actual type: Vector a ('S n0)
Relevant bindings include
takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m
(bound at takeWhileVector.hs:69:1)
In the expression: (x :- takeWhileVector f xs)
In an equation for ‘takeWhileVector’:
takeWhileVector f (x :- xs) = (x :- takeWhileVector f xs)
我本以为我的 takeWhileVector 类型定义如下：
对于所有类型 'a' 和 nat 种类，此函数 returns a 'Vector a m'，其中 'm' 是种类 Nat。
我是否需要将 takeWhileVector 的类型签名更改得更具体，以便显示结果是 Vector a (m :: Nat)？
否则，我该如何更改它以使其编译？
您建议的类型无法实现，即无人居住：
takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m
记住调用者选择类型变量a,n,m。这意味着调用者可以使用您的函数，例如
takeWhileVector :: (a -> Bool) -> Vector a Z -> Vector a (S Z)
这是胡说八道，因为如果你一开始就得到 none，你就不能产生一些 a。更实际的是，这个函数的调用者并不意味着能够选择有多少结果并传递一个完全不相关的函数——这与 takeWhile.
的预期语义不一致
我猜你的意思大概是
takeWhileVector :: (a -> Bool) -> Vector a n -> exists m. Vector a m
除了 exists 是无效的 Haskell 语法。相反，你需要像
这样的东西
data SomeVector a where
S :: Vector a m -> SomeVector a
takeWhileVector :: (a -> Bool) -> Vector a n -> SomeVector a
没有办法静态知道 Vec 由 takeWhileVec 编辑的 return 的长度：它取决于 Vec 中包含的值，并且你使用的功能。然而，我能做的是给你一个值，你可以模式匹配 learn Vec 的长度。输入 singleton values.
data Natty n where
Zy :: Natty Z -- pronounced 'zeddy', because I'm a limey
Sy :: Natty n -> Natty (S n) -- pronounced 'essy'
对于给定的 n 类型 Nat，恰好有一个（非 undefined）类型 Natty n 的值。因此，如果您对 Natty 有所了解，您也会了解其关联的类型级别 Nat。*
为什么我们不能使用 Nat 来达到这个目的？ Haskell 保持值和类型之间的分离。类型级别 Nat 与值级别 Nat 除了结构相似性外没有任何关系：值 S Z 的类型为 Nat，而不是 S' Z' - 所以我们必须使用 Natty，Nat 的第二个副本，手动将值和类型绑定在一起。 （真正的依赖类型系统，例如 Agda，允许您为值级和类型级计算重用相同的 Nat。）
*您也可以使用类型 类.
以其他方式传播知识
计划是 return 输出向量及其长度为 Natty，类型排列方式使 GHC 理解 Natty 确实如此表示它的长度。您可能首先考虑问题中示例的这种变化：
-- takeWhile :: (a -> Bool) -> Vec a n -> (Natty m, Vec a m)
但这并没有说对：我们是说 takeWhile 可以 return 调用者选择的任何 m，这是不正确的！它只能return由函数和输入向量确定的唯一m。正如我提到的，这在编译时是不可知的，所以我们必须对编译器保密长度。
data AVec a = forall n. AVec (Natty n) (Vec a n)
AVec 是一个 existential type: n appears on the right-hand side but not the left. This technique allows you to emulate a dependent pair type：Vec 的类型取决于 Natty 的值。只要数据的静态属性依赖于编译时不可用的动态信息，依赖对就很有用。
我们现在可以直接写takeWhile：
takeWhile :: (a -> Bool) -> Vec a n -> AVec a
takeWhile f Nil = AVec Zy Nil
takeWhile f (x :- xs) = case takeWhile f xs of
AVec n ys -> if f x
then AVec (Sy n) (x :- ys)
else AVec Zy Nil
我们不得不放弃 Vector 长度的静态知识，那么如何将 AVec 与对长度提出静态要求的函数一起使用呢？由于 AVec 的构造方式，我们知道左槽中的 Natty 表示右槽中向量的长度：它们都具有相同的（存在隐藏的）类型参数 n.因此，通过 Natty 上的模式匹配，我们了解了 Vec.
的长度
head :: Vec a (S n) -> a
head (x :- xs) = x
head' :: AVec a -> Maybe a
head' (AVec Zy Nil) = Nothing
head' (AVec (Sy n) xs) = Just (head xs)
在这个例子中，我们只关心向量是否比1长，所以Sy上的模式匹配足以向GHC证明我们应该被允许使用head。 （有关证明有关 AVec 的事实的更复杂示例，请参阅 a related answer of mine。）
@chi 提到了一个诱人的想法：您可能想证明由 takeWhile 编辑的向量 return 不长于输入向量。
takeWhile :: (a -> Bool) -> Vec a n -> AShorterVec a n
其中 AShorterVec 是不超过 n 的向量类型。我们的挑战是写下 AShorterVec.
的定义
给定两个自然数，你如何确定第一个小于或等于第二个？这种关系是归纳的。如果左操作数为零，则它自动小于或等于任何自然数。否则，如果一个数字的前身小于或等于另一个数字的前身，则该数字小于或等于另一个数字。我们可以使用 GADT 将其编码为建设性证明。
data LTE n m where
ZLte :: LTE Z m
SLte :: LTE n m -> LTE (S n) (S m)
如果 n 小于 m，您可以得出 LTE n m 的值。如果不是，则不能。这就是 Curry-Howard isomorphism 的意义所在。
现在我们准备好定义 AShorterVec：为了构建 AShorterVec a n 的值，您需要能够通过提供一个值来证明它比 n 短LTE m n。当您在 AShorterVec 构造函数上进行模式匹配时，它会返回证明，以便您可以使用它进行计算。
data AShorterVec a n = forall m. AShorterVec (LTE m n) (Vec a m)
takeWhile 编译时只有一个小改动：我们必须操作这个证明对象。
takeWhile :: (a -> Bool) -> Vec a n -> AShorterVec a n
takeWhile f Nil = AShorterVec ZLte Nil
takeWhile f (x :- xs) = case takeWhile f xs of
AShorterVec prf ys -> if f x
then AShorterVec (SLte prf) (x :- ys)
else AShorterVec ZLte Nil
另一种为 takeWhile 提供类型的方法是将长度的上限推入 return 类型本身，而不是将其作为数据携带。这种方法省去了与 Natty、LTE 等证明项和存在量化的任何争论。
data ShorterVec a n where
SNil :: ShorterVec a n
SCons :: a -> ShorterVec a n -> ShorterVec a (S n)
再一次，ShorterVec a n 表示不超过 n 的向量集。 ShorterVec 的结构让人联想到 finite sets，但从自然世界转换为向量世界。一个空向量比你想命名的任何长度都短； cons 单元将最小有效上限增加 1。请注意，n 的值永远不会完全由 ShorterVec 类型的值确定，因此您可以为 ShorterVec 提供任何有效的上限。这两个表达式都是类型正确的：
ok1 = SCons 1 (SCons 3 SNil) :: ShorterVec Int (S (S (S Z)))
ok2 = SCons 1 (SCons 3 SNil) :: ShorterVec Int (S (S Z))
但这一个不是：
-- notOk = SCons 1 (SCons 3 SNil) :: ShorterVec Int (S Z) -- the vector is longer than our stated upper bound.
使用此数据类型，您可以编写一个精美简单的 takeWhile 版本，它看起来与原始列表版本完全一样：
takeWhile :: (a -> Bool) -> Vec a n -> ShorterVec a n
takeWhile f Nil = SNil
takeWhile f (x :- xs) = if f x
then SCons x (takeWhile f xs)
else SNil
放宽我们对类型的假设使函数更易于实现，但您需要付出代价才能拥有另一种需要相互转换的类型。您可以通过测量长度从 ShorterVec 转换回使用依赖对的版本。
toAVec :: ShorterVec a n -> AVec a
toAVec SNil = AVec Zy Nil
toAVec (SCons x xs) = case toAVec xs of
AVec n ys -> AVec (Sy n) (x :- ys)
我们开始使用单例将类型和值绑定在一起，并使用存在类型将有关数据的运行时信息与数据本身包装在一起。然后，按照@chi 的想法，我们使用证明项将 takeWhile 的 正确性 （的一部分）编码到类型签名中。然后我们想到了一种方法，将长度不变量直接烘焙到 return 类型中，无需证明任何定理。
一旦您尝到了依赖类型编程的滋味，就很难再回到过去的方式了。富有表现力的类型系统给你至少三个优势：你可以编写其他语言不允许的有效程序（或强迫你重复代码）；您可以为相同的功能编写更有意义的类型，做出更有力的承诺；并且您可以通过机器可检查的方式证明程序的正确性。
不过，Haskell 还没有设置。一个问题是单例使绑定类型和值变得不必要地复杂：Nat-Natty 区别导致样板代码激增，其中大部分我已经为您省去了，在类型和值之间来回移动。 （这个样板文件的大部分内容都可以自动化 - 这就是 the singletons library 给你的。）如果我们想指定 takeWhile 正确性的另一个方面 - 事实上输出列表的所有元素都满足谓词 -我们必须专门处理单例列表和类型级谓词函数。我还发现每次我想要量化存在的东西时声明一个新的顶级类型很乏味（你可以编写库来帮助解决这个问题，尽管它们通常会产生其他样板文件）——我们缺乏类型级的 lambdas谢谢。另一个主要困难是限制什么可以使用 DataKinds 提升到类型级别：不能提升 GADT 和存在类型，所以例如你不能有一个多维数组，其形状被表达静态地作为 Vec Nat n。
没有真正的依赖类型系统使依赖类型如此难以使用！
Haskell 初学者。我定义了以下类型：
data Nat = Z | S Nat
data Vector a n where
Nil :: Vector a Z
(:-) :: a -> Vector a n -> Vector a (S n)
infixl 5 :-
我正在尝试编写函数 takeWhileVector，其行为与 takeWhile 在列表上的行为相同，但在向量上。
我的实现如下：
takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m
takeWhileVector f Nil = Nil
takeWhileVector f (x :- xs) = if (f x) then (x :- takeWhileVector f xs) else Nil
这不会编译并产生以下错误：
Could not deduce (m ~ 'S n0)
from the context (n ~ 'S n1)
bound by a pattern with constructor
:- :: forall a (n :: Nat). a -> Vector a n -> Vector a ('S n),
in an equation for ‘takeWhileVector’
at takeWhileVector.hs:69:20-26
‘m’ is a rigid type variable bound by
the type signature for
takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m
at takeWhileVector.hs:67:20
Expected type: Vector a m
Actual type: Vector a ('S n0)
Relevant bindings include
takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m
(bound at takeWhileVector.hs:69:1)
In the expression: (x :- takeWhileVector f xs)
In an equation for ‘takeWhileVector’:
takeWhileVector f (x :- xs) = (x :- takeWhileVector f xs)
我本以为我的 takeWhileVector 类型定义如下：
对于所有类型 'a' 和 nat 种类，此函数 returns a 'Vector a m'，其中 'm' 是种类 Nat。
我是否需要将 takeWhileVector 的类型签名更改得更具体，以便显示结果是 Vector a (m :: Nat)？ 否则，我该如何更改它以使其编译？
您建议的类型无法实现，即无人居住：
takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m
记住调用者选择类型变量a,n,m。这意味着调用者可以使用您的函数，例如
takeWhileVector :: (a -> Bool) -> Vector a Z -> Vector a (S Z)
这是胡说八道，因为如果你一开始就得到 none，你就不能产生一些 a。更实际的是，这个函数的调用者并不意味着能够选择有多少结果并传递一个完全不相关的函数——这与 takeWhile.
我猜你的意思大概是
takeWhileVector :: (a -> Bool) -> Vector a n -> exists m. Vector a m
除了 exists 是无效的 Haskell 语法。相反，你需要像
data SomeVector a where
S :: Vector a m -> SomeVector a
takeWhileVector :: (a -> Bool) -> Vector a n -> SomeVector a
没有办法静态知道 Vec 由 takeWhileVec 编辑的 return 的长度：它取决于 Vec 中包含的值，并且你使用的功能。然而，我能做的是给你一个值，你可以模式匹配 learn Vec 的长度。输入 singleton values.
data Natty n where
Zy :: Natty Z -- pronounced 'zeddy', because I'm a limey
Sy :: Natty n -> Natty (S n) -- pronounced 'essy'
对于给定的 n 类型 Nat，恰好有一个（非 undefined）类型 Natty n 的值。因此，如果您对 Natty 有所了解，您也会了解其关联的类型级别 Nat。*
为什么我们不能使用 Nat 来达到这个目的？ Haskell 保持值和类型之间的分离。类型级别 Nat 与值级别 Nat 除了结构相似性外没有任何关系：值 S Z 的类型为 Nat，而不是 S' Z' - 所以我们必须使用 Natty，Nat 的第二个副本，手动将值和类型绑定在一起。 （真正的依赖类型系统，例如 Agda，允许您为值级和类型级计算重用相同的 Nat。）
*您也可以使用类型 类.
以其他方式传播知识计划是 return 输出向量及其长度为 Natty，类型排列方式使 GHC 理解 Natty 确实如此表示它的长度。您可能首先考虑问题中示例的这种变化：
-- takeWhile :: (a -> Bool) -> Vec a n -> (Natty m, Vec a m)
但这并没有说对：我们是说 takeWhile 可以 return 调用者选择的任何 m，这是不正确的！它只能return由函数和输入向量确定的唯一m。正如我提到的，这在编译时是不可知的，所以我们必须对编译器保密长度。
data AVec a = forall n. AVec (Natty n) (Vec a n)
AVec 是一个 existential type: n appears on the right-hand side but not the left. This technique allows you to emulate a dependent pair type：Vec 的类型取决于 Natty 的值。只要数据的静态属性依赖于编译时不可用的动态信息，依赖对就很有用。
我们现在可以直接写takeWhile：
takeWhile :: (a -> Bool) -> Vec a n -> AVec a
takeWhile f Nil = AVec Zy Nil
takeWhile f (x :- xs) = case takeWhile f xs of
AVec n ys -> if f x
then AVec (Sy n) (x :- ys)
else AVec Zy Nil
我们不得不放弃 Vector 长度的静态知识，那么如何将 AVec 与对长度提出静态要求的函数一起使用呢？由于 AVec 的构造方式，我们知道左槽中的 Natty 表示右槽中向量的长度：它们都具有相同的（存在隐藏的）类型参数 n.因此，通过 Natty 上的模式匹配，我们了解了 Vec.
head :: Vec a (S n) -> a
head (x :- xs) = x
head' :: AVec a -> Maybe a
head' (AVec Zy Nil) = Nothing
head' (AVec (Sy n) xs) = Just (head xs)
在这个例子中，我们只关心向量是否比1长，所以Sy上的模式匹配足以向GHC证明我们应该被允许使用head。 （有关证明有关 AVec 的事实的更复杂示例，请参阅 a related answer of mine。）
@chi 提到了一个诱人的想法：您可能想证明由 takeWhile 编辑的向量 return 不长于输入向量。
takeWhile :: (a -> Bool) -> Vec a n -> AShorterVec a n
其中 AShorterVec 是不超过 n 的向量类型。我们的挑战是写下 AShorterVec.
给定两个自然数，你如何确定第一个小于或等于第二个？这种关系是归纳的。如果左操作数为零，则它自动小于或等于任何自然数。否则，如果一个数字的前身小于或等于另一个数字的前身，则该数字小于或等于另一个数字。我们可以使用 GADT 将其编码为建设性证明。
data LTE n m where
ZLte :: LTE Z m
SLte :: LTE n m -> LTE (S n) (S m)
如果 n 小于 m，您可以得出 LTE n m 的值。如果不是，则不能。这就是 Curry-Howard isomorphism 的意义所在。
现在我们准备好定义 AShorterVec：为了构建 AShorterVec a n 的值，您需要能够通过提供一个值来证明它比 n 短LTE m n。当您在 AShorterVec 构造函数上进行模式匹配时，它会返回证明，以便您可以使用它进行计算。
data AShorterVec a n = forall m. AShorterVec (LTE m n) (Vec a m)
takeWhile 编译时只有一个小改动：我们必须操作这个证明对象。
takeWhile :: (a -> Bool) -> Vec a n -> AShorterVec a n
takeWhile f Nil = AShorterVec ZLte Nil
takeWhile f (x :- xs) = case takeWhile f xs of
AShorterVec prf ys -> if f x
then AShorterVec (SLte prf) (x :- ys)
else AShorterVec ZLte Nil
另一种为 takeWhile 提供类型的方法是将长度的上限推入 return 类型本身，而不是将其作为数据携带。这种方法省去了与 Natty、LTE 等证明项和存在量化的任何争论。
data ShorterVec a n where
SNil :: ShorterVec a n
SCons :: a -> ShorterVec a n -> ShorterVec a (S n)
再一次，ShorterVec a n 表示不超过 n 的向量集。 ShorterVec 的结构让人联想到 finite sets，但从自然世界转换为向量世界。一个空向量比你想命名的任何长度都短； cons 单元将最小有效上限增加 1。请注意，n 的值永远不会完全由 ShorterVec 类型的值确定，因此您可以为 ShorterVec 提供任何有效的上限。这两个表达式都是类型正确的：
ok1 = SCons 1 (SCons 3 SNil) :: ShorterVec Int (S (S (S Z)))
ok2 = SCons 1 (SCons 3 SNil) :: ShorterVec Int (S (S Z))
但这一个不是：
-- notOk = SCons 1 (SCons 3 SNil) :: ShorterVec Int (S Z) -- the vector is longer than our stated upper bound.
使用此数据类型，您可以编写一个精美简单的 takeWhile 版本，它看起来与原始列表版本完全一样：
takeWhile :: (a -> Bool) -> Vec a n -> ShorterVec a n
takeWhile f Nil = SNil
takeWhile f (x :- xs) = if f x
then SCons x (takeWhile f xs)
else SNil
放宽我们对类型的假设使函数更易于实现，但您需要付出代价才能拥有另一种需要相互转换的类型。您可以通过测量长度从 ShorterVec 转换回使用依赖对的版本。
toAVec :: ShorterVec a n -> AVec a
toAVec SNil = AVec Zy Nil
toAVec (SCons x xs) = case toAVec xs of
AVec n ys -> AVec (Sy n) (x :- ys)
我们开始使用单例将类型和值绑定在一起，并使用存在类型将有关数据的运行时信息与数据本身包装在一起。然后，按照@chi 的想法，我们使用证明项将 takeWhile 的 正确性 （的一部分）编码到类型签名中。然后我们想到了一种方法，将长度不变量直接烘焙到 return 类型中，无需证明任何定理。
一旦您尝到了依赖类型编程的滋味，就很难再回到过去的方式了。富有表现力的类型系统给你至少三个优势：你可以编写其他语言不允许的有效程序（或强迫你重复代码）；您可以为相同的功能编写更有意义的类型，做出更有力的承诺；并且您可以通过机器可检查的方式证明程序的正确性。
不过，Haskell 还没有设置。一个问题是单例使绑定类型和值变得不必要地复杂：Nat-Natty 区别导致样板代码激增，其中大部分我已经为您省去了，在类型和值之间来回移动。 （这个样板文件的大部分内容都可以自动化 - 这就是 the singletons library 给你的。）如果我们想指定 takeWhile 正确性的另一个方面 - 事实上输出列表的所有元素都满足谓词 -我们必须专门处理单例列表和类型级谓词函数。我还发现每次我想要量化存在的东西时声明一个新的顶级类型很乏味（你可以编写库来帮助解决这个问题，尽管它们通常会产生其他样板文件）——我们缺乏类型级的 lambdas谢谢。另一个主要困难是限制什么可以使用 DataKinds 提升到类型级别：不能提升 GADT 和存在类型，所以例如你不能有一个多维数组，其形状被表达静态地作为 Vec Nat n。
没有真正的依赖类型系统使依赖类型如此难以使用！