The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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.