Thoughts on O'Labl O'Caml merge.

[John Prevost <prevost@maya.com>]

I was recently thinking about row polymorphism, structs and sum types.
It occurred to me that one could do row polymorphism with sum types as
well as with structs.  My model was something like this (thought it
requires a strange kinding system) (Well, it was too long, so I moved
it to the bottom.)


In any case, the point I have is that I came to the realization that
SML (while not allowing row polymorphism) has different (and smaller)
restrictions on the labels of struct types:

fun x { a : int, b : float } = a + round b

fun y { a : float, b : int } = a + float b

You can use the same labels in more than one way.

O'Caml, having taken a different road, requires that struct types be
defined ahead of time, and labels cannot overlap--just like the
current sum types in both languages.  I thought "Hmm, it might be
interesting to set up a language where this property is true of both
sum types and struct types, and then add row polymorphism to it."

Then I saw the messages about merging O'Labl and O'Caml, and started
looking at O'Labl again, and saw the row polymorphism on polymorphic
variants.

And that made me think: "So now O'Caml will have a system which allows
reusable sum labels, and non-reusable struct labels.  And SML will
have a system which has reusable struct labels but not reusable sum
labels."



Important questions:

So--the heart of my question: would it be possible to, while adding
row polymorphism on sum types (or a variation on that theme) also add
it on struct types (or a variation of that theme) outside of objects?


The only other thing I can think of which has been a thorn in my side
is the overreach of the value restriction on functional values--which
hurts a lot when you're doing stuff with purely functional or
otherwise safe combinators.  I don't know if this is open for
discussion, as it's been hashed over on the mailing list in the past,
but I suppose if things are being changed around, there might be a
possibility.





Here's the type system I was working on:

<type> ::= int
         | bool
         | { <label> : <type> }
         | [ <label> : <type> ]
         | <type> + type
         | <type> | <type> 
         | ... other base types, type constructors, etc.

(where that last pipe is a pipe symbol, not another option.  Silly
notation on my part.  :)

Actually, the + and | type operators need to have {} and [] types,
respectively, so:

|- bool : base

|- int  : base

|- { <label> : <type> } : struct

|- [ <label> : <type> ] : sum

|- <type1> : struct    |- <type2> : struct
------------------------------------------
      |- <type1> + <type2> : struct

|- <type1> : sum    |- <type2> : sum
------------------------------------
     |- <type1> | <type2> : sum

Which is a rather overcomplicated kinding system, but oh, well.  I was
just playing.  So, with this system and polymorphism, you could have:

{ a : int } + { b : float } + 'a

represents "any value that has at least fields a : int and b : float", and

[ a : int ] + [ b : float ] + 'a

represents "any value which has at least sum possibilities a : int and
b : float"

Other people have worked this out in better and greater detail than I
have, including the "at least" vs "no more than" issue for sum types.