Idris 中元组的智能构造函数

Question

我开始阅读“使用 Idris 进行类型驱动开发”的第 6 章，并尝试为元组向量编写智能构造函数。

TupleVect : Nat -> Type -> Type
TupleVect Z _ = ()
TupleVect (S k) a = (a, TupleVect k a)

someValue : TupleVect 4 Nat
someValue = (1,2,3,4,())

TupleVectConstructorType : Nat -> Type -> Type
TupleVectConstructorType n typ = helper n
  where
    helper : Nat -> Type
    helper Z = TupleVect n typ
    helper (S k) = typ -> helper k

tupleVect : (n : Nat) -> (a : Type) -> TupleVectConstructorType n a
tupleVect Z a = ()
tupleVect (S Z) a = \val => (val, ())
tupleVect (S (S Z)) a = \val2 => \val1 => (val2, val1, ())
-- ??? how to create tupleVect (S k) a

如何为任意 k 创建构造函数？

Answer 1

我对 Idris 几乎一无所知，只知道它是一种 dependently-typed、Haskell-like 语言。但是我觉得这个问题很有趣，所以我试了一下。

显然你需要一个递归的解决方案。我的想法是使用一个额外的参数 f 来累积函数到目前为止已经吃掉的 val1..val_n 参数。当达到基本情况时，返回 f。

tupleVectHelper Z a f = f
tupleVectHelper (S n) a f = \val => tupleVectHelper n a (val, f)

tupleVect n a = tupleVectHelper n a ()

我不知道这是否有效，我还没有弄清楚如何编写 tupleVectHelper 的类型，但我已经尝试手动替换 n = 3 并且它似乎确实在纸上解决了，尽管生成的元组是倒退的。但我认为这不应该太难解决。

希望对您有所帮助！

Answer 2

基本上是@Matthias Berndt 的想法。倒数要添加的箭头，同时使最终元组更长。为此，我们需要从 TupleVectType.

访问更宽松的助手

TupleVectType' : Nat -> Nat -> Type -> Type
TupleVectType' Z n a = TupleVect n a
TupleVectType' (S k) n a = a -> TupleVectType' k (S n) a

TupleVectType : Nat -> Type -> Type
TupleVectType n = TupleVectType' n Z

tupleVect : (n : Nat) -> (a : Type) -> TupleVectType n a
tupleVect n a = helper n Z a ()
    where
        helper : (k, n : Nat) -> (a : Type) -> (acc : TupleVect n a)
            -> TupleVectType' k n a
        helper Z n a acc = acc
        helper (S k) n a acc = \x => helper k (S n) a (x, acc)

someValue2 : TupleVect 4 Nat
someValue2 = (tupleVect 4 Nat) 4 3 2 1

但请注意，这将导致 \v2 => \v1 => (v1, v2, ()) 而不是 \v2 => \v1 => (v2, v1, ())，因为前者更符合 TupleVect (S k) a = (a, TupleVect k a) 的递归定义。

Idris 中元组的智能构造函数

Smart constructor for tuple in Idris

haskell

idris