Idris Dependent Pairs: Unexpected behavior between compiled program and REPL

Question

When practicing using dependent pairs in Idris, I have encountered an unexpected difference in behavior between compiled programs and the REPL. The following datatype is what I am testing with:

(a : Type ** b : Type ** Arrow a b)

Which should represent some relation between type a and type b. Given an instance of the above, I would like to extract the "proof" term of the type. I can do this from the REPL with DPair.snd $ DPair.snd <some-instance> and everything works fine. However, if I try to make a function:

unwrap : (a ** b ** Arrow a b) -> Arrow a b
unwrap x = DPair.snd $ DPair.snd x

the program will compile, but will fail when I try to call it. The error message returned is

(input): No such variable b

Has anyone encountered this or knows of a solution?

Answer 1

What you want to achieve is not possible. If you look at the type of unwrap : (a1 : Type ** b1 : Type ** Arrow a b) -> Arrow a b you see that it uses a different datatype than (a : Type ** b : Type ** Arrow a b). That's because the arguments a, b are quantified beforehand - setting the resulting type (which is also the difference to the REPL case; there you aren't bound to the arguments). So with :set showimplicit it is

Main.unwrap : {b : Type} -> {a : Type} ->
              (a1 : Type ** b1 : Type ** Main.Arrow a b) ->
              Main.Arrow a b

That's the thing about dependent pairs, you can't restrict them easily. Take a look at Vect.filter : (elem -> Bool) -> Vect len elem -> (p : Nat ** Vect p elem) - if we had a function like unwrap : (p : Nat ** Vect p elem) -> Vect p elem, we wouldn't need dependent pair in the first place.

Instead, a function that would call unwrap would need to inspect p and then handle the Vect accordingly. Sadly, we can't easily inspect types (at least if you want to generalize for all types). So your best bet is: don't use dependent types here.

Answer 2

I realise I'm a year and a half late, but... This absolutely is possible! You just need to remember that the type a ** P is just syntactic sugar for DPair a (\x => P a); in the latter form, nothing special is going on whatsoever and so you can use your a and b just like you'd expect. We can also gain insight from how DPair.snd is typed in the standard library:

Idris> :t DPair.snd
snd : (x : DPair a P) -> P (fst x)

So, to extract the a-value from our pair, we simply call fst on that pair. How intuitive! (fst itself simply has the type DPair a P -> a). To get the b-value, which is the first value of the second part of our pair, we call fst . snd on the outermost pair. Therefore, your function should look like:

unwrap : (x : DPair a (DPair b . Arrow)) -> Arrow (fst x) (snd $ fst x)
unwrap x = snd (snd x)

(or, equivalently:)

unwrap : (x : DPair a (\theA => DPair b (\theB => Arrow theA theB))) -> ...

For whatever reason, unwrap = DPair.snd . DPair.snd doesn't work... but that's not too much of an issue.