我可以将列表转换为带有类的长度索引向量吗？ [英] Can I convert a list to a length indexed vector with a class?
问题描述
为了避免参差不齐的矩阵，我想设计一个包含长度类型的列表的类型包装器。 （请纠正我，如果我不应该称之为长度索引向量。）我想提供它作为具有智能构造函数的抽象类型，其中将是一个
这是我的地方：
数据Nat = Z | S Nat
data Vector（n :: Nat）a = Vector [a]导出显示
v0 ::向量Z a
v0 =向量[]
put :: a - >向量n a - >向量（S n）a
放入x（向量xs）=向量（x：xs）
class折叠一个
类型Elem a
fold :: [ Elem a] - > a
实例折叠（向量Z a）其中
类型Elem（向量Z a）= a
折叠[] = v0
实例折叠向量（S n）a）其中
类型Elem（向量（S n）a）= a
倍（x：xs）=放x（倍xs）
Fold typeclass应该从列表中逐个获取元素，把放到vector中。我打算代表基本情况的实例以及沿着 Nat urals进行结构化归纳的归纳情况。然而，
然而， ，我发布的代码不起作用，我无法排除错误。实质上，它讨论了不同长度的向量的元素类型不相等：
...
预期类型：[Elem（Vector na）]
实际类型：[Elem（Vector（'s n）a）]
...
fold（x：xs）= put x（fold xs）
^^
如果我假设神奇的强制功能：
fold（x：xs）= put x（fold $ undefined xs）
- 然后我会遇到另一个错误：
由于使用'fold'而产生的折叠（向量na））
...
fold（x：xs）= put x（fold $ undefined xs）
^^^^^^ ^^^^^^^^^^^^^
这令我伤心，因为它意味着我
- 可以使用我获得了一个
I sList这样的实例吗？ - 我可以获得它吗？
- 打通我。我是否认为正确的方向？我怎么能说出依赖类型可行的方面，哪些不是，以便我可以判断这个特定案例的易处理性，以及我自己将来可能面对的其他情况？
编译器通知您两个不同的问题。 b $ b
从本质上讲，它讨论了不同长度的向量的元素类型不相等：
Spot on！你在这里有两种方法。如果你想保持 Elem 系列作为typeclass的一部分，你必须在归纳情况下添加一个额外的约束，基本上告诉GHC我的元素类型是相等的 ：
instance（Elem（Vector na）〜a）=>折叠（向量（S n）a）其中
类型Elem（向量（S n）a）= a
折叠（x：xs）=放置x（折叠xs）
或者，您可以将此类型系列完全分开，并且只有一个（更明智的）实例：
type family Elem xs :: *
类型实例Elem（Vector nx）= x
class fold a where
fold :: [Elem a] - > a
由您决定！
这让我感到悲伤，因为它意味着我的归纳实例不会迭代。
确保它不会迭代，因为你还没有告诉GHC去找到递归子问题！
- 如果您决定保留类型系列关联的
实例（Elem（Vector na）〜a，Fold（Vector na））=>折叠（向量（S n）a）其中
类型Elem（向量（S n）a）= a
折叠（x：xs）=放置x（折叠xs）
或
- If您决定不保留类型家族关联的
实例Fold（Vector na）=> Fold（Vector（S n）a）其中
fold（x：xs）= put x（fold xs）
To avoid ragged matrices, I want to design a type wrapper for lists that holds length in type. (Please correct me if I should not call it a "length-indexed vector".) I would like to provide it as an abstract type with smart constructors, among which would be an IsList instance or something similar in spirit.
This is where I am:
data Nat = Z | S Nat
data Vector (n :: Nat) a = Vector [a] deriving Show
v0 :: Vector Z a
v0 = Vector [ ]
put :: a -> Vector n a -> Vector (S n) a
put x (Vector xs) = Vector (x:xs)
class Fold a where
type Elem a
fold :: [Elem a] -> a
instance Fold (Vector Z a) where
type Elem (Vector Z a) = a
fold [ ] = v0
instance Fold (Vector (S n) a) where
type Elem (Vector (S n) a) = a
fold (x:xs) = put x (fold xs)
The Fold typeclass is supposed to take elements from a list one by one and put them to the vector. The instances I intend to represent the base case and the inductive case for structural induction along the Naturals.
However, the code I posted does not work, and I cannot sort the errors out. In essence, it talks about the element types of vectors of different length not being equal:
...
Expected type: [Elem (Vector n a)]
Actual type: [Elem (Vector ('S n) a)]
...
fold (x:xs) = put x (fold xs)
^^
If I assume the magical coercion function:
fold (x:xs) = put x (fold $ undefined xs)
− I will then reach another error:
• No instance for (Fold (Vector n a)) arising from a use of ‘fold’
...
fold (x:xs) = put x (fold $ undefined xs)
^^^^^^^^^^^^^^^^^^^
This saddens me because it must mean my inductive instance does not iterate.
I need help with this.
- Can I obtain an
IsListinstance this way? - Can I obtain it at all?
- The point of dependent typing does not seem to get through to me. Do I think in the right direction at all? How can I tell what is doable with dependent types and what is not, so that I can judge the tractability of this particular case, and other cases that I may face in the future, by myself?
The compiler is informing you of two different problems.
In essence, it talks about the element types of vectors of different length not being equal:
Spot on! You have two approaches here. If you want to keep the Elem family as part of the typeclass, you'll have to add an extra constraint to the inductive case basically telling GHC "my element types are equal":
instance (Elem (Vector n a) ~ a) => Fold (Vector (S n) a) where
type Elem (Vector (S n) a) = a
fold (x:xs) = put x (fold xs)
Alternately, you could make that type family completely separate and have only one (more sensible) instance:
type family Elem xs :: *
type instance Elem (Vector n x) = x
class Fold a where
fold :: [Elem a] -> a
Up to you!
This saddens me because it must mean my inductive instance does not iterate.
Sure it doesn't "iterate", because you haven't told GHC to go find a recursive subproblem! Just add that subproblem to your constraint for the inductive case.
-- If you decided to keep the type family associated
instance (Elem (Vector n a) ~ a, Fold (Vector n a)) => Fold (Vector (S n) a) where
type Elem (Vector (S n) a) = a
fold (x:xs) = put x (fold xs)
or
-- If you decided not to keep the type family associated
instance Fold (Vector n a) => Fold (Vector (S n) a) where
fold (x:xs) = put x (fold xs)
这篇关于我可以将列表转换为带有类的长度索引向量吗？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
