[TYPES] union types and overloading

[Johan Nordlander]

>> Note that the declaration of type Both is necessary in this system.
>> Note also that the argument to constructor B is still of type T1, even
>> when B is considered a constructor of type Both.
>
> My plan roughly agrees with O'Haskell's design decision, except for 
> one thing:
> the Both declartion from the programmer. Quick question: for what did
> you trade the no-extra-annotation? (Maybe I have to study your papers, 
> but for
> quick answers...)
>
> All the best,
>
> -Kwang

Hi Kwang,

I actually haven't thought of it as an extra annotation.  Type Both 
simply represents a node in the partial order of nominal subtyping, 
just as T1 and T2 do.  In general, an O'Haskell type definition lists 
zero or more base types, together with zero or more constructors (in 
the case of datatypes) or selectors (in the case of records).

The goal with the O'Haskell type system was to mimic the type modeling 
features of object-oriented languages like Java as closely as possible, 
with the addition of parametric polymorphism, co/contravariance, 
automatic type inference, and extensible algebraic datatypes.  Because 
of my focus on human readability, going for the full power of 
intersection and union types was never an option.  It also seems like 
"going just a little bit" in that direction is problematic enough.

For one thing, adding a sum operator to denote type extension would 
make the subtyping relation between "a" and "a+b" dependent on whether 
"a" and "b" stand for records or datatypes.  Alternatively, the sum 
operator could be restricted to datatypes, but then polymorphism would 
have to be restricted accordingly.  Moreover, one could argue that with 
a sum operator, any combination of constructors forms a valid 
pattern-matching domain type, thus reducing the status of datatype 
names to mere abbreviations (i.e., structural subtyping).  I based my 
work on the assumption that nominal subtyping is preferable, both in 
the interest of reabability, and for the purpose of improving error 
detection.

All the best,
Johan