Update of "First-Class Labels"
Not logged in

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview

Artifact ID: 5c9f2fe7856767fab90d15142b44e4876b8cf157
Page Name:First-Class Labels
Date: 2015-07-11 22:23:51
Original User: neilmadden
Mimetype:text/x-markdown
Parent: 7a3a184af02fb781beda40527df73c385667ef74
Content

First-Class Labels

Part of me wants to make SiCL statically typed, or at least informed by typing discipline so that that door is open in the future. One very interesting approach is that of first-class labels described in the linked paper.

We can think of the fields in a record and the tags in an algebraic data type (variant) as individual objects in their own right. These can be polymorphic in the type of value that can be associated with them. For example, we might have two different record types in our program with a "name" field - one takes a simple string, while the other takes a complex Name object (with first-name, last-name, title, etc fields). The "name" field would be shared between them, with a type like (in ML-style postfix type notation):

val name : a Label

i.e., name is a label that can take any type of value. We can then define operations over labels to construct records etc. For example, the '=' infix operator extends a record with a new field value:

{ _ = _, ... } : ∀r,l,a. (r\l) => a -> r... -> a Label -> {l : a, r...}

This (in slightly odd syntax) says that to assign a value to some field in a record that may contain other fields, then firstly r must "lack" (r\l) an "l" field already, and then given a value of type "a", a record r, a label of type "a Label" (i.e., matching the type of value), then we return a record with the new label l of type a, and the remaining record r (using row typing).

This looks complicated, but it's a really nice and simple idea. In particular, it provides a typing discipline (and reasonably efficient compilation strategy) for having first-class symbols in the language with a lot of flexibility on how they are used - for records and objects, for first-class messages, for algebraic datatypes, etc. You can even assign labels to variables, pass them as arguments to functions (and return them), store them in data structures, etc.

I therefore propose adding a first-class label concept to SiCL, either dynamically typed or statically so (static typing would require row typing, which is nice but by no means simple).

Label constants are created using a macro postfix colon operator that converts the preceding identifier or string into a label - thus foo: and "foo": are labels (the same label in this case). This ensures a natural syntax for both variants and record fields.

Variant types can then be formed as a sum of labels:

type MyType = a: | b:(x,y) | c:

Such a type is closed by default. We could also allow open variant types where additional labels can be passed:

type MyType = a: | b:(x,y) | c: | ...

(The "| ..." is the actual syntax here). This indicates that functions taking a value of this type can expect any of the given variants or any other variant label at all (and must include default cases in matching etc).

Likewise for records:

type MyRecord = { x: Int, y: Text }

is a fixed type record, while

type MyRecord = { x: Int, y: Text, ... }

allows additional fields to be present.

A label is itself a function that takes a value of the appropriate type and returns a Field of that type:

type a Label = a -> a Field

Thus, the expression x: is a label while (x: 12) is an integer field (Int Field). (x: Int) is a Type Field (or Label field, given that Int must be a label?).

Pattern Matching

As described in the paper, pattern matching variants using first-class labels is incredibly simple as you just pass a record using the same labels as fields and functions of the correct type for values and then just select the field of the given variant label:

type a Option = some: a | none:
val x = some: 12
match x {
    some: n -> n + 1,
    none: 0
}

If we also allowed an initial upper-case letter to indicate a label, then we could write that as follows:

type a Option = Some a | None
val x = Some 12
match x {
    Some x -> x + 1,
    None 0
}

As labels take a single argument, we could define nullary labels like None as implicitly taking a () argument. Then the above match could be written as:

match x {
    Some x -> x + 1,
    None _ -> 0
}

This provides a pleasing symmetry. How do we handle default cases? Via row polymorphism:

type Cases = A | B | ...
match case {
    A _ -> stuff,
    B _ -> stuff,
    ... -> default
}

The type of "match" is then

val match :: ∀r,a. <r> -> {to a r} -> a

where <r> means a variant of the row r (e.g., A | B | ...) and "to" is a recursive type operation that is defined by induction over the row type r, ensuring that every label is mapped to a function producing a value of type a, i.e., b -> a.

There is an analogous function for records that takes a variant argument:

val recElim :: ∀r,a. {r} -> <to a r> -> a

This effectively allows us to implement field selection:

(.) :: r\l => {l :: a, r...} -> Label l -> a
r.l  = recElim r <l = x -> x>

Another nice point is that if we make Fields implements equality only considering the label equality, then records just become sets of fields, as duplicate fields would then be disallowed. Equality for the record itself could still be defined in terms of the field values.