Re: [isabelle] subtype definition in Isabelle



On Fri, 15 Jan 2016, 刘涛 wrote:

I am wondering if Isabelle supports subtype definition , something just like subclass and superclass in C++.

If you look at the latest and greatest developments of the "object-oriented" approach in Scala, namely "traits", they approximate an idea of structured algebraic specifications from the good old times.

In Isabelle you can work in that style with "locales".

There is a particularly useful view on locales called "type classes". This allows to work in the manner and style of Haskell (the classic version of 1998, without recent additions).


And the subtype inherits the attributes of the parent-type.

If you mean plain record types with structural subtyping (in the sense of Hindley-Milner polymorphism) then the HOL "record" package will do that. But it is not as frequently used as one might think.


	Makarius


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