Stream: Coq users

Topic: Dependent types of applicative functions?

Alessandro Bruni (Oct 14 2022 at 09:41):

Hi all, I'm trying to encode the type of a function that takes an arbitrary number of parameters, do you know if this is possible in Coq?
Here is what I have:

Fixpoint Op (n : nat) :=
    match n with
    | 0 => nat
    | S m => nat -> (Op m)
    end.

Fixpoint serveOp (n : nat) (op : Op n) :=
    match n with
    | 0 => op
    | S m => serveOp m ((op: Op (S m)) 0)
    end.

Parsing this code fails with the following error:

In environment
serveOp : forall n : nat, Op n -> Op n
n : nat
op : Op n
m : nat
The term "op" has type "Op n" while it is expected to have type "Op (S m)".
Not in proof mode.

Do you know if there is something equivalent to this that works?

Pierre-Marie Pédrot (Oct 14 2022 at 09:44):

You just have to write a commutative cut like this:

Fixpoint serveOp (n : nat) : Op n -> nat :=
    match n with
    | 0 => fun op => op
    | S m => fun op => serveOp m ((op: Op (S m)) 0)
    end.

Pierre-Marie Pédrot (Oct 14 2022 at 09:44):

as a rule of thumb if you pattern match on something and something else depends on it, you should perform a commutative cut

Pierre-Marie Pédrot (Oct 14 2022 at 09:45):

(notably CPDT uses a generic pattern called "the convoy pattern" for this kind of stuff)

Janno (Oct 14 2022 at 09:49):

A word of caution: usually you have to annotate the return type of the match. Coq let's you get away without that only when the function is well-typed. While you are building it you'll get nonsense error messages unless you explicitly add the type annotation: match n as n return Op n -> nat with.

Pierre-Marie Pédrot (Oct 14 2022 at 09:52):

Indeed, writing dependent functions is an arcane art. I'd recommend using Equations if you want to follow that path further.

Alessandro Bruni (Oct 14 2022 at 10:10):

Uhm, I see, thanks for the help!

Michael Soegtrop (Oct 14 2022 at 10:18):

@Pierre-Marie Pédrot : do you have references on the wording "commutative cut" for this technique?

Pierre-Marie Pédrot (Oct 14 2022 at 10:22):

The expression comes from the λ-calculus community, but I'm afraid I don't have a precise reference.

Pierre-Marie Pédrot (Oct 14 2022 at 10:24):

The English translation of Girard's Proofs and Types calls them "commuting conversions".

Enrico Tassi (Oct 14 2022 at 12:10):

Aren't commutative cuts more about reduction than typing? Here the problem is that the type to be "rewritten" in not under the match

Enrico Tassi (Oct 14 2022 at 12:16):

In a sense here typing forces you to put the lambda under the match, so if the first argument is not a concrete number you can't fire the beta redex for the sencond one. Commutative cuts (moving the lambda outside the match) would allow the beta (but break typing in a system like Coq which has dependent types). If it was simlpe-typed, then permuting match with fun would be more safe, IMO.

Pierre-Marie Pédrot (Oct 14 2022 at 12:19):

The usage in the dependent type community is clearly abusive: these cuts do not commute. But they have the shape of the typical commutative cut (i.e. a λ-cut blocked by a ι-redex), hence the name.

Enrico Tassi (Oct 14 2022 at 12:54):

OK, so let's forge the word "non-commutative cut" and stick to it ;-)

Last updated: Apr 18 2024 at 18:01 UTC