Email Gateway (Aug 22 2022 at 12:07): Email Gateway (Aug 22 2022 at 12:07):From: 刘涛 <liut@ios.ac.cn>
Hi,
I am wondering if Isabelle supports subtype definition , something just like subclass and superclass in C++.
And the subtype inherits the attributes of the parent-type.
Thanks.
Tao Liu
Email Gateway (Aug 22 2022 at 12:08):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 25 2024 at 20:15 UTC