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?
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.
as a rule of thumb if you pattern match on something and something else depends on it, you should perform a commutative cut
(notably CPDT uses a generic pattern called "the convoy pattern" for this kind of stuff)
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.
Indeed, writing dependent functions is an arcane art. I'd recommend using Equations if you want to follow that path further.
Uhm, I see, thanks for the help!
@Pierre-Marie Pédrot : do you have references on the wording "commutative cut" for this technique?
The expression comes from the λ-calculus community, but I'm afraid I don't have a precise reference.
The English translation of Girard's Proofs and Types calls them "commuting conversions".
Aren't commutative cuts more about reduction than typing? Here the problem is that the type to be "rewritten" in not under the match
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.
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.
OK, so let's forge the word "non-commutative cut" and stick to it ;-)
Last updated: Jan 28 2023 at 05:02 UTC