Re: [isabelle] type_synonym




Am 10/08/2012 16:37, schrieb Makarius:
> 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.

And it would not buy us very much, except:

>> 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?

Check in the sense of ascertain, test, verify. Writing T down and having it
parsed settles only that it (T) is a legal type, but not if it is, for example,
a field.

Tobias





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