Monomorphism, monomorphism...

[Carl R. Witty]

"Marcin 'Qrczak' Kowalczyk" <qrczak@knm.org.pl> writes:

> 09 Oct 2001 13:55:04 -0700, Carl R. Witty <cwitty@newtonlabs.com> pisze:
> 
> > The TREX paper from Mark Jones and Benedict Gaster (I hope I
> > have the names right) had both extensible records and extensible
> > variants (extensible variants being what you would need to implement
> > downcasts),
> 
> I don't think so. Here is how the requirement can be formulated:
> 
> We need some type T such that it's possible to define a family of
> functions for arbitrary choices of A:
>     upA   :: A -> T
>     downA :: T -> Maybe A
> satisfying downA (upA a) = Just a. We want to choose the type for T
> before deciding the exact set of types for A.

It is true that extensible variants do not give you a single, closed
type T with this property.  

However, I think it is likely that any program you wanted to write
using these functions could instead be written in a system with
extensible variants.  Functions would be polymorphic over the exact
variant type, and the typechecker would stitch together all the
requirements on the variant type so that when compiling "main", it
could decide what the actual type was.  (I say "likely" because I'm
not certain that the type inference described in the Gaster/Jones
paper would work the way I want it to, since I've never used a system
that implemented extensible variants.)

Carl Witty