Unions¶
Basic Unions¶
Unions are a nominal type which is used to specified alternatives.
union Maybe[T] {
| Nothing
| Just of T
}
fun show[T] (x:Maybe[T]) =>
match x with
| Nothing => "Nothing"
| Just v => v.str
endmatch
;
var x = Just 1;
println$ show x;
The fields of a union are usually called constructors. Constructors may be either constant constructors like Nothing above, or non-constant constructors like Just, which take an argument.
Pattern matching is used as shown to decode a value of union type. Matches consist of an argument and a list of branches. Each branch contains a pattern and a handler.
In the Some branch the pattern variable v is set to 1 in the example, and converted to a string in the handler expression.
Pattern matching selects the first branch with a pattern that matches and evaluates the corresponding handler.
Generalised Algebraic Data Types¶
Felix also provides generalised algebraic data types, or GADTS: A GADT is a polymorphc union with a per constructor existential constraint on the type variable.
union pair[T] =
| PUnit of unit => pair[unit]
| Pair[T,U] of U * pair[T] => pair[U * pair[T]]
;
var x1 = #PUnit[unit];
var x2 = Pair (22,x1);
var x3 = Pair (99.76,x2);
fun f[T:GENERIC] (x:T) = {
match x with
| Pair (a,b) => return a.str + ","+b.f;
| PUnit => return "UNIT";
endmatch;
}
println$ f x3;
With a GADT, some components may have a RHS after the => symbol which must be the union type subscripted with a constraint on the type variables: in the example the PUnit constructor returns a pair with parameter T constrained to type unit, whereas the Pair constructor introduces and existential parameter T, and returns a pair with type argument pair[U * pair[T]].
This particular construction can be used to recursively define a heterogenous list similar to a system tuple type, but amenable to recursive analysis by a generic function such as f above. The analysis requires polymorphic recursion which Felix does not support directly but in this case can be emulated by a generic function which is expanded by the compiler to a nest of specialised functions.