Idris中如何构建包含多元素的依赖元组？

Great question! The (**) syntax sugar works perfectly for binary dependent pairs, but when you need multi-element tuples where later components depend on earlier ones (not just the initial value), nesting dependent pairs is the way to go—regular tuples fall short here because they don’t let subsequent types reference the specific values of prior elements.

Why Regular Nested Tuples Fail #

Your initial workaround (x : Int ** (Positive x, IsEven x)) works when both predicates only depend on x, but it can’t handle cases where a later component needs to reference the instance of an earlier dependent type (not just the base value x). For example, if you had a type that depends directly on a Positive x instance (not just x itself), regular tuples can’t capture that dependency.

The Correct Approach: Nested Dependent Pairs #

Instead of regular tuples, nest (**) pairs so each new component can reference all previously bound variables. Let’s walk through an example where a third component depends on the second:

First, define a type that depends on a Positive instance:

data DependsOnPositive : Positive x -> Type where
  ValidDep : Positive x -> DependsOnPositive x

Now, we can create a three-element dependent tuple where the third component relies on the second Positive instance:

v3 : (x : Int ** (p : Positive x ** DependsOnPositive p))
v3 = (2 ** (SucIsPositive OneIsPositive ** ValidDep (SucIsPositive OneIsPositive)))

Here’s what’s happening:

• The first pair binds x : Int and its proof p : Positive x.
• The nested pair then uses p to define the type of the third component (DependsOnPositive p), so the third value must be a valid instance of that type tied directly to p.

A More Complex Example #

Let’s extend this to a four-element tuple where the fourth component depends on both the second and third elements. First, define a type that compares two Positive values:

data IsGreater : Positive a -> Positive b -> Type where
  GtSuccessor : IsGreater (SucIsPositive n) n

Now create the tuple:

v4 : (x : Int ** 
       (p : Positive x ** 
         (y : Int ** 
           (q : Positive y ** IsGreater p q))))
v4 = (3 ** 
       (SucIsPositive (SucIsPositive OneIsPositive) ** 
         (2 ** 
           (SucIsPositive OneIsPositive ** GtSuccessor))))

Here, the final IsGreater p q type references both p (the proof for 3) and q (the proof for 2), which only works because we nested each dependent pair to bind those variables.

Key Takeaways #

• Use nested (**) pairs for multi-element dependent tuples where later components depend on earlier values or their proofs.
• Each nested pair lets you bind a new variable that subsequent types can reference, enabling arbitrary depth of dependencies.
• Reserve regular tuples (a, b) for cases where all components only depend on the outermost variable (like your original (Positive x, IsEven x) example).

内容的提问来源于stack exchange，提问作者luochen1990