Stream: Coq users

Topic: Dependent types of applicative functions?


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Alessandro Bruni (Oct 14 2022 at 10:10):

Uhm, I see, thanks for the help!

view this post on Zulip Michael Soegtrop (Oct 14 2022 at 10:18):

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

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Oct 14 2022 at 10:24):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Oct 14 2022 at 12:54):

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


Last updated: Jan 28 2023 at 05:02 UTC