Re: [isabelle] type_synonym

On Fri, 10 Aug 2012, Tobias Nipkow wrote:

I figured it out myself: because in an application to some type T, "T t = T :: field", but the rhs is only legal if T is a type variable, not a compound type. Hence my type synonym would only make sense if we allowed types of the form "T :: C" (just like we allow terms of the form "e :: T"). I had not thought this through, but by analogy with the term level, I guess "T::C" should be rejected if T is not of class C.

Correct. The term language as full type constraint solving, but the type language not. Sort constraints are limited to type variables, and there is no "sort inference".

In the past 2 decades I have occasionally observed the difference as a matter of fact. I don't think it would be feasible to change this.

Although I had not originally thought of this generalization, I must say that I have occasionally wished I could write "T :: C" to check if some type is in some class. But maybe there is alternative way to check this?

Once you write down T as expression, its type variables have already some sort assignment, so it is all settled.

What exactly means "to check"?  What is the application context?


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