Re: [isabelle] Problems with coercions



Hi Akihisa,

> On 4 Oct 2017, at 12:31, Yamada, Akihisa <Akihisa.Yamada at uibk.ac.at> wrote:
> 
> Dear Dmitriy,
> 
>> It is the other way round: the show statement yields "sr :: real" annotations (since sr is fixed in the context). In the lemma statement "sr" is just a free type variable and its precise type is the result of type inference.
> 
> ah, I see. So if I understand correctly, coercion is performed before 
> the type inference, and its behavior will change when types are inferred.

Chapter 3 of the implementation manual (isabelle doc implementation) gives a high-level overview of how type checking/inference work in Isabelle. Coercion inference is implemented as a "check phase" and runs quite early in the stack of check phases. (Most check phases assume their input to be well-typed, while the coercion inference tries to repairs badly-typed terms. For well-typed terms, coercion inference behaves as plain Hindley-Milner type inference.)

>> I guess you are not surprised that the following fails (fortunately):
>> 
>> lemma
>>   "f x = x"
>> proof -
>>   define f :: "'a â 'a" where "f = id"
>>   show "f x = x" unfolding f_def by simp
>> qed
> 
> Definitely not, because everyone sees that `define f' will define f. I 
> hope not all Isabelle users have to understand the behavior of coercion 
> mechanismâ

I'd say all users of coercions (not equal to all Isabelle users) need to understand what they are "buying into" by using coercions:

- coercion inference will not modify type-correct terms
- for not type-correct terms it will try to repair them using the coercions it knows
- in case there are different ways to repair a term, one way will be chosen (the choice depends on the input term*)

The potential ambiguity makes it necessary to carefully inspect the terms and if needed to manually adjust them by adding type annotations or coercion functions.

Cheers,
Dmitriy

[*] To be very precise: the input term that coercion inference receives when the user writes a string s in the context ctxt is:

     s
     |> Syntax.parse_term ctxt
     |> singleton (snd o Proof_Context.prepare_sorts ctxt)
     |> singleton (fst o Type_Infer_Context.prepare_positions ctxt)
     |> singleton (snd o Type_Infer_Context.prepare ctxt)







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.