Lambda the Ultimate

I was initially motivated by a desire to model "Noneable" sort of like C, and not like ML's 'a Option or Haskell's Maybe a.

Wanting to distinguish a type Person from ?Person, I don't want None to be a kind of automatic bottom type of all (ref?) types. So "Noneable" looks like a union, in fact, a union of a type and a distinguished value, None.

In my syntax, it would look something like this (where enum defines variants and Or is a primitive of the type language).


enum NONE is | None;
type ? 'a = Or 'a None;


Wanting to not make this a special case, I was wondering if such union types present any difficulties so long as all values carry type tags in any case. So we might define Num thusly.

type Num = Or Int Dbl;


Carrying type tag info, the values are distinguishable using pattern matching. For the "Noneable" case, we have.


fun 'a not-none-or-dflt (?'a, 'a -> 'a)
| None, dflt = dflt
| v, _ = v;


Using Scala style type test syntax, we might write for Num:


fun toint(Num -> Int)
| x:Int = x
| d = Math.round(d);


My thinking is that values' type tags are already like automagical constructors, hence no need to write:


enum Val is
| aInt(Int);
| aDbl(Dbl);
| aStr(Str);
....
etc.


Am I missing some grand glaring whole in such a "true union" type construct given my tagged values? Any other languages have a similar type system feature that I might look at?

Thanks much.

Scott