Hi guys,
Wondering if you might have an idea:
In Typer, the basic datastructure is the "algebraic datatype" (which
combines a sum, product, and recursion), and the basic eliminator is the
"pattern matching case".
It works OK, but is unsatisfactory:
1- both of those are fairly large/complex.
2- it means that extracting a record field is a "case" operation that
discards all but the required field, so it's an O(n) operation (where
n is the size of the record), if not in the final code, at least in
intermediate code.
3- it means the choice of representation of datatype tags is hardcoded
in the blackbox compiler.
While point n°2 might seem irrelevant, it is a pain with large records,
such as those you might get when records are used to represent modules:
the encoding of the simple "String.concat" reference ends up taking
space proportional to the number of primitives exported from the
"String" module, which can be rather large.
I'd like to find another option and was thinking of something along the
following lines:
- provide a separate product primitive.
- provide a "union" type, i.e. an *untagged* sum.
- provide primitive discrimination operations, such as "dispatch on an Int".
then the Either type could look like
Either a b = union (Singleton(1), a)
(Singleton(2), b)
and
case e
| Left x => ...
| Right y => ...
would turn into
switch (e.0 <withmagicproof>)
| 1 => let e' = cast (Singleton(1), a) e;
x = e'.1
in ...
| 2 => let e' = cast (Singleton(2), b) e;
y = e'.1
in ...
Obviously, we'd still want to have "case", but written as a macro.
The `magicproof` is needed to convince Typer that all union members have
a field 0. And of course, each `cast` would also need to provide
a proof (constructed from a proof provided by `switch`) that indeed we
know that `e` is this specific member of the union.
The way I presented it is fairly general, but pretty heavyweight to
define and to use: every "case" will be compiled to that big
switch-with-proofs and the definition of a "record selection out of
a union" (such as the "e.0 <withmagicproof>") seems fairly complex
as well.
Does anyone here have another approach to suggest?
Stefan
