Re: [isabelle] type_synonym

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.

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?


Am 09/08/2012 22:55, schrieb Makarius:
> On Thu, 9 Aug 2012, Tobias Nipkow wrote:
>> type_synonym 'a t = "'a :: field"
>> yields
>> Ignoring sort constraints in type variables(s): "'a"
>> in type abbreviation "t"
>> Why that? It would be very nice not to lose them.
> Can you explain what you are trying to achieve? Do you want the system to reject
> type expressions if the argument types of synonyms do not observe the sort
> constraint?
> Type classes never restrict the domain of type constructors, they are always
> defined.  Type synonyms are not even type constructors, just some abstract
> syntax for existing types.
>     Makarius

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