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