The Coq mailing list

[t x <txrev319 AT gmail.com>]

Is https://gist.github.com/anonymous/7100956 correct?

Where error (1) is fixed at line 18 and error (2) is fixed at line 21.

"I find the prose difficult to understand" wasn't meant to criticize the writing, but to mean "I can't derive pseudocode from these paragraphs."

Pierre:

  (1) What do you mean I'm missing Parameters?

  (2) What do you mean by

> Nope again

> fun x_1 … x_n y => RExpr has to be well typed (else Coq would have JMEq_eq !)

On Tue, Oct 22, 2013 at 6:19 AM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

On 10/22/2013 05:36 AM, t x wrote:

Suppose now, instead of trying to understand "how to use Coq", we are interested in "how to implement a verifier" then is the following pseudocode correct ?

(* let matchExpr = entireity of the following block *)
match (expr) in y as T x_1 x_2 .. x_n return RExpr with
  | C1 y1_1 y1_2 ... y1_m1 => D1
  | C2 y2_1 y2_1 ... y2_m2 => D2
  ...
  | Ck yk_1 yk_2 ... yk_mk => Dk
end

then, we can say that:
  * matchExpr has type RExpr/{y=expr}
if:
  forall 1 <= i <= k, we have:
    normalize(RExpr/{y=Ci yi_1 ... yi_mi}) = normalize(Di)

-- and this is actually all there is to it, no?

Just to give an alternative response to Pierre's, at a more conceptual level:
No.  Your rule both (1) uses an invalid "pun" between a term and its type and (2) ignores the [as] clause completely (and actually you've switched [in] and [as] above, so morally speaking it's [in] that you ignore).

To fix (1), replace "normalize(Di)" with normalization of the _type_ of "Di" in the appropriate context.
To fix (2), subsitute for the "x_i" variables, too, in the appropriate places.

I think you're finding that, as you struggle to show that the explanation in CPDT is "unnecessarily complex," your increasingly correct approximations are converging toward what is already in CPDT, but written in a way that will be more confusing to newcomers. ;)  I believe that any experienced Haskell or OCaml programmer would already consider the description in CPDT to be a clear explanation of how to implement this rule in a type-checker.