Dependent Tuple in Idris?

Question

It's easy to write down a dependent pair in Idris with the "**" syntax sugar:

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)

But When I want to put more things into the tuple, I failed (the following code causes error):

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

So, generally, what should I do when I want to put more than 2 element into the Dependent Pair (Tuple) ?

I find that I can use a nested normal tuple to do that in this case:

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

But this is limited. When the third part is depending on the second one, this no longer works.

So I'm still wondering what is the suggested way to do that?

since you want a nested dependent pair you need to give a name to the second component: v3 : (x : Int ** foo : Positive x ** IsEven x) — Anton Trunov
@AntonTrunov Thank you, I think that's the answer. Hope you can post this as an answer so I can close this question. — luochen1990

Anton Trunov Anton Trunov · Accepted Answer · 2018-01-08T16:23:18

If the type of the third component of your dependent tuple does not depend on the value of the second component, then non-dependent pair as you have shown is the way to go.

In case you want a nested dependent pair you need to give a name to the second component:

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

Dependent Tuple in Idris?

1 Answers