Union Types for Haskell!?

Bernd Holzmüller holzmueller@ics-ag.de
Fri, 24 Nov 2000 11:02:11 +0100


Dies ist eine mehrteilige Nachricht im MIME-Format.
--------------82B6A52F122BE8F7263D41DD
Content-Type: text/plain; charset=iso-8859-2
Content-Transfer-Encoding: 8bit

I am about to finish my PhD, where I used the Vienna Definition Language
(VDL) to specify the semantics of some programming language constructs.
In order to verify this semantics description using a type checker and
by dynamic execution, I found and used Haskell as the language of choice
to map the VDL description to Haskell. I was quite impressed about the
expressive power of Haskell (e.g. the list comprehension syntax and the
use of the functions "any" and "all" together with ad-hoc definable
lambda-abstractions) and the flexible type system, which together
allowed me to almost literally transcribe the VDL description into
Haskell. Since then, I have used Haskell to build several parsers and
compilers for simple script languages as well as for other purposes.

There is one thing I was really missing in all these projects: the
existence of union types (i.e. the union of value sets of two existing
data types), for two reasons:

- Firstly, to map VDL union types to Haskell, I needed to introduce one
further indirection, using another data type with one special type
constructor for each former variant. This was actually the biggest
inconvenience in transforming VDL to Haskell. 

- Secondly, after having built abstract tree representations of
languages while parsing, I did want to traverse and manipulate such
trees (consisting of nodes belonging to several different data types)
for semantic analysis and code generation several times. Unfortunately,
I was not able to use a single function to map over the different nodes
of the abstract syntax tree. The only viable solution I found was to use
a set of functions, one for each node type, and to pass the whole set
down the tree, extracting and applying the appropriate function for each
node (type). To define one Haskell data type that defines each of the
different nodes as one variant would of course lead to much less type
safety, because each reference to a node would be much less precise/less
informative.

When I got to know Haskell, I was expecting a construct for union types
like:

  data B = ...
  data C = ...
  type A = B | C | D -- A accepts values of either B or C or D (cf. the
"Either a" type in the Prelude)

but this is not valid Haskell. Is there any reason for this restriction
in the Haskell type system? Does this lead to losing the principal type
property? And, if so, would you please give me an example where the
principal type does not exist any more when introducing union types in
the form above? Do any papers exist about this topic? Is there any
Haskell compiler supporting union types? Are there any considerations of
integrating union types into the Haskell type system, at least for
explicit type annotations (if type inference using union types should in
any way be problematic)?

I find the existence of union types very attractive. Apart from enhanced
flexibility in modelling, type error messages would possibly be more
traceable, because different branches in if- or case-expressions would
have the *same* relevance, rather than the first branch being
type-checked becoming normative for all other branches.

Thanks in advance,

Bernd Holzmüller
ICS AG
Sonnenbergstraße 13
70184 Stuttgart
++49 711 21037 0
holzmueller@ics-ag.de
--------------82B6A52F122BE8F7263D41DD
Content-Type: text/x-vcard; charset=iso-8859-2;
 name="holzmueller.vcf"
Content-Transfer-Encoding: 7bit
Content-Description: Visitenkarte für Bernd Holzmüller
Content-Disposition: attachment;
 filename="holzmueller.vcf"

begin:vcard 
n:Holzmüller;Bernd
tel;fax:0711-21037-75
tel;work:0711-21037-31
x-mozilla-html:FALSE
url:http://www.ics-ag.de
org:ICS AG;TS-TBV
adr:;;Sonnenbergstraße 13;Stuttgart;BW;70184;Deutschland
version:2.1
email;internet:holzmueller@ics-ag.de
fn:Bernd Holzmüller
end:vcard

--------------82B6A52F122BE8F7263D41DD--