Keith Wansbrough writes:
> > class Subtype sub super where
> > up :: sub -> super
> > down :: super -> Maybe sub
>
> See the extensible union types of [Sheng Liang, Paul Hudak and Mark
> Jones: Monad Transformers and Modular Interpreters]
>
> From the abstract:
>
> "... Finally, we have implemented our interpreter in Gofer,
> whose constructor classes provide just the added power over
> Haskell's type classes to allow precise and convenient
> expression of our ideas. This implementation includes a method
> for constructing extensible unions and a form of subtyping that
> is interesting in its own right."
>
> They have a multiparameter type class SubType, with methods `inj' and
> 'prj', just as you describe, implemented in Gofer.
Thanks for the pointer! The "class Subtype" component of my proposal
is a corroboration that that form of subtyping is interesting in its
own right. :-)
The other major components, then, are the insistence on a most
specific common supertype (MSCS) wherever there are common supertypes,
and the treating up of unificands to their MSCS when necessary.
Incidentally, I'll continue to use the terms `treating up and down'
instead of `injection and projection', because some subtyping is not a
matter of removing summands or adding record fields. Every square is
a polygon, but we may want to represent polygons as lists of points
and squares as pairs of points (opposite corners).
> I used this in my Masters thesis,
Should there be a printed copy available in some reading room at
Auckland University?
Regards,
Tom