Idris 中的依赖元组？

Question

在 Idris 中使用“**”语法糖很容易写下依赖对：

data Positive : Int -> Type where
    OneIsPositive : Positive 1
    SucIsPositive : Positive i -> Positive (i+1)

data IsEven : Int -> Type where
    ZeroIsEven : IsEven 0
    Add2IsEven : IsEven i -> IsEven (i+2)
    Sub2IsEven : IsEven i -> IsEven (i-2)

v1 : (x : Int ** Positive x)
v1 = (1 ** OneIsPositive)

v2 : (x : Int ** IsEven x)
v2 = (2 ** Add2IsEven ZeroIsEven)

但是当我想往元组中放入更多的东西时，我失败了（以下代码导致错误）：

v3 : (x : Int ** Positive x ** IsEven x)
v3 = (2 ** SucIsPositive OneIsPositive ** Add2IsEven ZeroIsEven)

那么，一般来说，当我想将2个以上的元素放入依赖对（元组）时应该怎么做？

我发现在这种情况下我可以使用嵌套的普通元组来做到这一点：

v3 : (x : Int ** (Positive x, IsEven x))
v3 = (2 ** (SucIsPositive OneIsPositive, Add2IsEven ZeroIsEven))

但这是有限的。当第三部分依赖于第二部分时，这不再有效。

所以我仍然想知道建议的方法是什么？

Answer 1

如果您的依赖元组的第三个组件的类型不依赖于第二个组件的值，那么您所显示的非依赖对就是要走的路。

如果您想要嵌套的 dependent 对，您需要为第二个组件命名：

v3 : (x : Int ** unusedName : Positive x ** IsEven x)

Idris 中的依赖元组？

Dependent Tuple in Idris?

dependent-type

idris