The Coq mailing list

[Randy Pollack <rpollack0 AT gmail.com>]

Thanks Guillaume, that was informative.

> Casts have no computational meaning, they are just meant as hints
> (and even then, the type checker tends to ignore them unless they ask
>  for a specific reduction machinery, so they are basically just hints for
> the pretyper).

Then why isn't casting removed from the typechecked terms in my example?

Best,
Randy
--


On Wed, Apr 29, 2015 at 10:33 AM, Guillaume Melquiond
<guillaume.melquiond AT inria.fr>
 wrote:
> On 29/04/2015 11:11, Randy Pollack wrote:
>>
>> This "answer" doesn't explain either of the observations I asked about:
>>
>>> Type inference is as you would expect: Γ |- t : A  /\ A =c B ----> Γ |-
>>> (t
>>> :c B) : B. The :c can be just regular kernel conversion or call to a VM
>>> (bytecode or native). Reduction ignores casts entirely (AFAICT).
>>
>>
>> Type inference apparently causes eta-expansion of the term t, but
>> Matthieu's purported type inference rule doesn't change t.
>
>
> Type inference does not cause eta-expansion, per se. But type coercion does.
> Your term is somehow ill-typed, since cons has type "Type ->" while your
> cast forces it to have type "Set ->". So the pretyper performs an
> eta-expansion.
>
> Disclaimer: I am no specialist of Coq's type system, and it might well be
> that, according to the typing rules, the term is well-typed, even without an
> eta-expansion. But the pretyper at least seems to think it needs to put an
> eta-expansion there for the term to be well-typed.
>
>> Apparently reduction causes the cast "term constructor" to be dropped,
>> at least in some cases, which is not the same as ignoring casts
>> entirely.
>
>
> Casts have no computational meaning, they are just meant as hints (and even
> then, the type checker tends to ignore them unless they ask for a specific
> reduction machinery, so they are basically just hints for the pretyper). As
> a consequence, they can be dropped or ignored or whatever.
>
>> Finally, consider again the goal command
>>
>>     Goal (cons: forall (A:Set), A -> list A -> list A) = cons.
>>
>> Coq shows the goal to be
>>
>>      ((fun A : Set => cons (A:=A)):forall A : Set, A -> list A -> list A)
>> =
>>      (fun A : Set => cons (A:=A))
>>
>> Why is the RHS eta-expanded?
>
>
> Because of type coercion, again. Since both sides of the equality are
> supposed to have the same type, and since the left-hand side has type "Set
> ->" (because of your explicit cast), the pretyper of Coq decides to coerce
> the right-hand side to this type using an eta-expansion.
>
> Best regards,
>
> Guillaume
>