[isabelle-dev] »real« considered harmful

[Larry Paulson]

On 5 Jun 2015, at 22:22, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> 
>> Why do we need abbreviations such as these?
>> 
>> abbreviation real_of_nat :: "nat \<Rightarrow> real”
>>  where "real_of_nat \<equiv> of_nat"
>> 
>> abbreviation real_of_int :: "int \<Rightarrow> real”
>>  where "real_of_int \<equiv> of_int"
>> 
>> abbreviation real_of_rat :: "rat \<Rightarrow> real”
>>  where "real_of_rat \<equiv> of_rat"
>> 
>> abbreviation complex_of_real :: "real \<Rightarrow> complex"
>>  where "complex_of_real \<equiv> of_real"
> 
> The deeper reason why these have been introduced is that such
> conversions of type T => 'a::c can be difficult to write in presence of
> type ambiguities.  If you need more special types, you can do barely
> anything else than writing »(of_foo x :: T)« which clutters readability.

OK — but that’s no reason to introduce “real” as another way to write these coercions, while introducing precisely the sort of type ambiguity that is the root of such problems.

Conceivably we could introduce a prefix syntax for type constraints, e.g.

	[:real:]of_nat k

I’d find such a thing useful from time to time.

Larry