嵌套对练习

Question

的 ch6 练习

练习 3 个状态：

We could implement a vector as nested pairs, with the nesting calculated from the length. For example:
TupleVect 0 ty = ()
TupleVect 1 ty = (ty, ())
TupleVect 2 ty = (ty, (ty, ()))
Define a type level function TupleVect which implements this behaviour. Remember to start with the type of TupleVect. When you have the correct answer, the following definition will be valid:
test : TupleVect 4 Nat
test = (1,2,3,4,())

这是我想出的：

TupleVectType : Nat -> (a : Type) -> Type
TupleVectType Z     _ = ()
TupleVectType (S n) a = (a, TupleVectType n a)

TupleVect : (n : Nat) -> a -> TupleVectType n a
TupleVect Z _     = ()
TupleVect (S n) a = (a, TupleVect n a)

我认为足够了，但是，MyTupleVect 4 Nat错了：

*Exercises> TupleVect 4 Nat
(Nat, Nat, Nat, Nat, ()) : (Type, Type, Type, Type, ())

但是，如果我提供实际值，即不是 Type，它 returns:

*Exercises> TupleVect 4 True
(True, True, True, True, ()) : (Bool, Bool, Bool, Bool, ())

请告诉我如何更正此 TupleVect 函数以匹配预期输出。

我不清楚如何提供 TupleVect 4 Nat，然后枚举 Nat，但从 1 开始，而不是 0。

Answer 1

您对 TupleVectType 的定义实际上是 TupleVect 应该是的。该练习要求您实现一个函数 TupleVect，其中 returns type of n-ary tuple-represented vectors。

您对 TupleVect 的定义是通常所谓的 replicate 的实现，它通过复制 将单个 x : a 转换为向量 repeat x : Vect n a ]n次。

总而言之，根据您的定义，将按预期进行以下类型检查：

foo : TupleVectType 4 Nat
foo = (1, 2, 3, 4, ())

所以我建议将 TupleVectType 重命名为 TupleVect。

嵌套对练习

Nested Pairs Exercise

idris