git.haldean.org ubik / 02a5277 docs / adt-inst.txt
02a5277

Tree @02a5277 (Download .tar.gz)

adt-inst.txt @02a5277raw · history · blame

Instantiating Algebraic Data Types =====================================
Haldean Brown                                      First draft: May 2016
                                                  Last updated: May 2016

Status: Obsolete
        This document dates back from when everything was pairs of
        words; now that tuples are a base type, ADTs are just tuples.

------------------------------------------------------------------------

Algebraic data types are translated at compile time into value-encoded
heterogenous lists which, in combination with the actual type
declaration itself, give the runtime sufficient type information to be
able to work with the types.

The ADT definition itself is also compiled down to a value encoding.
ADT declarations are essentially three lists: type parameters, parameter
constraints and constructor definitions (for more information, see
docs/type-decls.txt). The top level encoding is:

        (name (type-params (constraints (constructors (0 0)))))

The sub-structures have the following form:

        type-params : (type-param ... (type-param (0 0)))
        type-param : value-encoded string of parameter name

        constraints : (constraint ... (constraint (0 0)))
        constraint : (value-encoded string of parameter name,
                      value-encoded type constraint)

        constructors : (constructor ... (constructor (0 0)))
        constructor :
            (ctor-name (first-param-type (second-param-type (... (0 0)))))

The instantiations are just tuples, essentially, where the first item is
a string that represents the constructor used for the instantiation, and
the remaininig items are all the arguments to the constructor (i.e., the
fields of the object). These can be unpacked and addressed using the
native function ubik-adt-get, which takes an instantiation and an index
and returns the object at that index.

As a concrete example, take this:

        ^ Entity = Person Name
        : print-name = \(Person n) -> emit n

The ADT itself is compiled down to the following definition:

        : Entity ^ Type = (
            # No type params
            (0 0)
            # No constraints
            ((0 0)
            # One constructor
             ("Person" (Name (0 0))))
        )

The print-name function is compiled down to this Ubik source:

        : print-name = \x -> {
            : n = ubik-adt-get x 0
            ! emit n
        }

For construction of ADTs, functions representing the type's constructors
are inserted into the environment. From the above example, the following
function would be created:

        : Person ^ Entity = \name -> ubik-adt-new-1 Entity "Person" name

The -1 at the end of ubik-adt-new-1 is a workaround for the lack of
variable-arity functions in Ubik; arglists are supported for up to 32
elements, meaning that an ADT can only have 32 fields.