Re: [Caml-list] Polymorphic Variants

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: Tom <tom.primozic@gmail.com>
> On 17/01/07, Jacques GARRIGUE <garrigue@math.nagoya-u.ac.jp> wrote:
> > From: Tom <tom.primozic@gmail.com>
> > > So... why actually are polymorphic variants useful? Why can't they
> > simply be
> > > implemented as normal, concrete (or how would you call them? ...)
> > variants?
> >
> > The original motivation was for the LablTk library, where some types
> > (index for instance) have lots of small variations. At that point
> > there where several options
> > * overloading (but ocaml loathes overloading, you could say that the
> >   total absence of overloading is essential to the language)
> 
> Is there a reason for that? Is it only hard to implement or are there any
> conceptual / strategical / theoretical reasons?

There are two kinds of theoretical reasons.

The most theoretical one is about semantics: with generic overloading,
all your semantics must take types into account. This is a problem as
most theoretical studies of lambda-calculus are based on so-called
erasure semantics, where types are discarded at execution. So this
means you must design your own, more complex semantics. Not that this
reason may not apply to constructor or record overloading, if you do
not allow the semantics to change according to the type.

The other one is about type inference. Basically, overloading has a
huge impact on overloading. The direct way to handle it, using types
alone, is deeply disruptive, as it means that some programs will be
refused for lack of type information. It is very hard to define a
clear criterion on which programs should be refused, notwithstanding
internal details of the compiler. This also applies to record and
constructor overaloading. There are other approach the problem, with
constrained type variables (either Haskell's type classes or G'Caml's
generic type variables,) but of course they add complexity to the type
system. And it is not clear that they solve the problem for
constructor and record overloading: in Haskell, records fields are not
overloaded, and constructor overloading has to be done by hand for
each type, through an explicit encoding into type classes.

Both reasons have practical impact. For the first one, using erasure
semantics means that the programmer also can discard types when
understanding the runtime behaviour of a program. For the second one,
you can write code that is maximally polymorphic, without too much
fear about the impact of performance (equality is overloaded, so
it still matters...) or strange ambiguity-related error messages.

So for the time being ocaml keeps to no overloading at all.

> > OCaml does not, as far as I know, have any structural typing for
> > records..

Not for records, but for objects. From a type-theoretic point of view
they are just equivalent.

> Hm... Actually, what I had in mind is nominal subtyping... similar to
> objects, in fact, objects in C++-like languages, just that they have no
> class methods.

Reading the description below, this all looks nice, independently of
the semantics limitation described above. However, you can kiss
farewell to type inference. With such an extensive overloading, you
would need type annotations all over the place.
By the way, this all looks likes the "used this feature in C++"
syndrome. Sure C++ is incredibly powerful. But it is built on rather
shaky theoretical fundations. So you can't expect to bring everything
from C++ to a new language. Why not think about new ways to solve
problems :-)
(To be completely honest, this also looks a bit like ML2000, and the
Moby language, which has a sound theoretical fundation, but never
really took off. You might want to go see for yourself.)

Jacques Garrigue
 
> Now... close your eyes (but try to continue reading this ;) ) and imagine
> you're in a dreamworld. You are programming in a language that has
>   * function overloading that allows you to have
>        length "abcd" + length [1; 2; 3]
>   * Constructor overloading, eliminating the need of
>        type parse_expression =
>            Pexp_name of string
>          | Pexp_constant of constant
>          | Pexp_let of (pattern * parse_expression) * parse_expression
>          | Pexp_apply of parse_expression * parse_expression list
>          | Pexp_try of parse_expression * (pattern * parse_expression) list
> 
>        type typed_expression =
>            Texp_ident of ident
>          | Texp_constant of constant
>          | Texp_let of (pattern * typed_expression) * typed_expression
>          | Texp_apply of typed_expression * typed_expression list
>          | Texp_try of typed_expression * (pattern * typed_expression) list
>     as it can be coded as
>        type parse_expression =
>            Name of string
>          | Constant of constant
>          | ...
> 
>        type typed_expression =
>            Ident of ident
>          | Constant of constant
>          | ...
> 
>   * nominal subtyping of records, with overloaded field names:
>        type widget = {x : float; y : float; width: float; height: float} (*
> top-level type *)
>        type button = {widget | text : string }
>        type checkbox = {button | checked : bool}
>        type image = {widget | url : string}
> 
>        type vector = {x : float; y : float}
>        type document {url : url}
> 
>     so subtypes could be applied to a function
>        fun move : widget -> (float * float) -> unit
> 
>        let chk = {x = 0.0; y = 0.0; width = 10.0; height = 12.0; text =
> "Check me!"; checked = false}
>        move chk (3.0, 3.0)
>     and types could be "discovered" at runtime:
>        let draw widget =
>          typematch widget with
>              w : widget -> draw_box (w.x, w.y, w.height, w.width)
>            | b : button -> draw_box (b.x, b.y, b.height, b.width); draw_text
> b.text
>            | i : image -> draw_image i.url (i.x, i.y)
>            | ...
> 
> Do you think you would be "satisfied" even without polymorphic variants?
> 
> I am not saying this just for fun... I want to create a language with
> overloading, but I kinda don't really like polymorphic variants... thou if
> they turn out to be really useful, I would probably start to like them.
> 
> Any comments?
> 
> - Tom