Ubik Type Declarations =================================================
Haldean Brown First draft: May 2016
Last updated: May 2016
Status: In progress
Remaining:
- Type aliases (not useful until type inference is complete)
- Interfaces
------------------------------------------------------------------------
There are three varieties of type declaration currently supported by the
Ubik specification:
1. Type aliases
2. Algebraic Data Types (ADTs)
3. Interfaces
Type aliases -----------------------------------------------------------
Type aliases are declared using the bind operator, much like a normal
binding:
: RowId = Integer
This establishes RowId as an alias for Integer. An alias is
unidirectional; given the alias ": A = B", a value of type A can be used
as a B, but a B cannot be used as an A.
An alias automatically inherits all of the interface implementations of
the aliased type. The inherited implementations can be overridden by
specifying a more specific implementation of the interface (see section
3).
The full grammar of type aliases is:
type_alias : TYPE_NAME IS type_expr
Algebraic Data Types ---------------------------------------------------
Algebraic Data Types (ADTs) are specified using the type operator. At
their simplest, ADTs are just like tuples:
^ Row = Row RowId Key Value
This specifies a new ADT called "Row" with a single constructor that
takes a RowId, a Key, and a Value. Multiple constructors can be given:
^ Solid
= Sphere Vector Double
= Box Vector Vector
= Cylinder Vector Vector Double
There is no correspondence between the name of the type and the name of
the constructors; for those coming from an OO-oriented language, each
constructor can be thought of as concrete subclasses of the abstract
ADT.
To make things even more interesting, an ADT can take other types as
parameters; this allows for things like strongly-typed containers or
other applications in which generics are useful. For example, you could
define a generic list type as:
^ List t
= Cons t List
= Nil
which is, coincidentally, exactly how Lists are defined. If you're
looking for multiple parameters, you just specify multiple variables:
^ Mapper a b = Func (a -> b) (List a)
This defines a Mapper type with a Func constructor, which takes a
function that maps one type to another, along with a list of the first
type. If you want to get really fancy, you can place constraints on the
types of the variables using the given and exists operators:
^ EqualPair a b
| ' Eq a
| ' Eq b
= EqualPair a b
In this example, the type can only be constructed if there are
implementations of Eq for both of the two arguments.
The full grammar of ADTs is:
adt_def
: TYPE TYPE_NAME type_params constraints ctors
type_params
: NAME type_params | %empty
constraints
: GIVEN EXISTS TYPE_NAME names constraints
| %empty
names
: NAME names
| %empty
ctors
: ctor ctors
| ctor
ctor
: IS TYPE_NAME parameters
parameters
: type_atom parameters
| OPEN_PAR type_expr CLOSE_PAR
| %empty
Interfaces -------------------------------------------------------------
Interfaces are lists of methods that types can implement. Interfaces
are often called "type classes" in other functional languages, but in my
experience calling them "classes" only serves to confuse people who are
used to object-oriented programming, where "class" is something more
like a "record".
Interfaces are specified using a combination of the interface and member
operators:
_ Numberish a
. add ^ a -> a -> a
. mult ^ a -> a -> a
Once specified, you can implement the interface by specifying an
implementation, using the defines and member operators:
~ Numberish Integer
. add = \x, y -> iadd x y
. mult = \x, y -> imult x y
~ Numberish Float
. add = fadd
. mult = fmult
You can then define methods that accept any type that implements an
interface:
: square
^ x -> x | ' Numberish x
= \x -> mult x x
Interfaces can also take parameters, because why not:
_ Evaluable x res
. eval ^ x -> res
Implementations must explicitly specify concrete types for the type
parameters of the interface being implemented:
_ Evaluable String (Maybe Integer)
. eval = \x -> read-string x
Just like ADTs, constraints on the type variables can be specified:
_ NumberList x a
| ' Numberish a
. get ^ x -> Index -> a
. sum ^ x -> a
You can then implement this with:
~ NumberList (List Integer) Integer
. get = list:get
. sum = reduce iadd 0
The full grammar of interface definitions is:
interface_def
: INTERFACE TYPE_NAME type_params constraints members
type_params
: NAME type_params | %empty
constraints
: GIVEN EXISTS TYPE_NAME names class_constraints
| %empty
names
: NAME names
| %empty
members
: MEMBER NAME TYPE type_expr members
| %empty
The full grammar of interface implementations is:
impl_def
: DEFINES TYPE_NAME parameters members
parameters
: type_atom parameters
| OPEN_PAR type_expr CLOSE_PAR
| %empty
members
: MEMBER NAME IS expr