Notes on Implementing Algebraic Subtyping

Algebraic Subtyping is a type system devised by Stephen Dolan in 2016, in his dissertation. It extends Hindley-Milner with subtyping, in a way that preserves decidability and principality. Over the past few years, I have implemented Algebraic Subtyping in my language Pinafore (omitting record types). Pinafore is, as far as I know, currently the only language to implement this type system besides Dolan’s own MLsub prototype.

These notes are mostly things I wish I knew when writing it. Not having a strong background in type theory, I did not necessarily understand every part of Dolan’s paper before implementing it, but just started work as I understood it. I have learnt a lot since then.

Awesomenesses

So what’s so great about Algebraic Subtyping?

Intuitiveness

When people interpret and understand the world, we use types, and we make wide use of subtype relations. “X is a dog”, “Y is a cat”, “Z is an animal”, and then, “every cat is an animal”, and so forth. That’s a subtype relation. And you might think that covariance and contravariance are esoteric type-theory concepts, but it turns out that they too are reflected in language: covariance with the word “of” (a bowl of apples is a bowl of fruit), and contravariance with the word “for” (a bowl for fruit is a bowl for apples). It’s therefore helpful to bring these concepts that are already intuitive into the formal type system of a programming language. For example, every text document is a document, every check box is a UI widget, etc.

Cleanliness

So of course “object-oriented” languages such as C++, C#, Java, and so forth already have subtyping. However, the type systems of these languages are marred by extraneous complexity. They are not elegant when considered abstractly, making them difficult to reason about. For example, they typically separate “primitive” and “reference” types that behave differently in certain ways; the unit type `void` is often not a first-class type; type polymorphism is often rather ad-hoc; and there’s no account of contravariance and covariance of type constructors. And the concept of function types tends to be particularly poorly implemented.

Scala is somewhat better, the type system is perhaps as good as it can be, but it’s ultimately limited by the underlying Java VM type system.

Algebraic Subtyping, by contrast, is what type-theorists think of as a real type system. It’s mathematically clean, making it much easier for both language developers and their users to reason about, and much less likely to involve unpleasant surprises.

Flexibility

Subtype relations in Algebraic Subtyping do not need to be injective, and no inverse conversions need to be provided. If `P` is a subtype of `Q`, (written `P <: Q`) then there is implicitly a conversion function from `P` to `Q`, but there does not need to be a retraction function `Q -> Maybe P`.

This is particularly valuable if you opt for non-uniform representation (below). The only thing that matters is that the subtype system is consistent. I give a proper definition of this below, but essentially it means that all subtype “paths” from `P` to `Q` are the same conversion. Provided you enforce that consistency, you can let your users create whatever systems of subtypes they want.

In a sense, Algebraic Subtyping disassembles the notion of “object orientation” into its underlying type-theory parts: subtyping, retractions, function types, constructor functions, etc.

Awkwardnesses

What’s not so great about Algebraic Subtyping? Or at least, what problems will you have to tackle?

Polar Types

In Algebraic Subtyping, certain constructions (`|`, `None`) are only allowed in positive position, and certain others (`&`, `Any`) are only allowed in negative position. So right away the user needs to pay attention to type polarity. For example, when a type is the argument of a function, its polarity is inverted (because the argument parameter of the function type constructor is contravariant), so its own parameters are also inverted. This can be a little tricky to get used to.

Non-Variant Parameters

In Algebraic Subtyping, every parameter of every type constructor must be either covariant or contravariant, and this creates subtype relations for the constructor. For example, if `P <: Q`, then `List P <: List Q`, because the type parameter of the `List` type constructor is covariant.

But some types might naturally want to be parameterised by a variable that is neither covariant nor contravariant. An obvious example is a reference cell, with “get” (covariant) and “set” (contravariant) operations. The (perhaps only mildly awkward) solution Algebraic Subtyping suggests, and Pinafore implements, is to use a contravariant/covariant pair of parameters. Pinafore has a special `{-p,+q}` syntax for this, but essentially they are nothing more than two parameters. For example:

``````type Cell {-p,+q}
newCell: p -> Action (Cell p)  # note "Cell p" is the same as "Cell {-p,+p}"
getCell: Cell {-p,+q} -> Action q
setCell: p -> Cell {-p,+q} -> Action Unit``````

Pinafore’s special syntax brings its own surprises:

``````f: WholeModel +a -> WholeModel +a = fn x => x;  # causes a type error

# looks like the same type on either side, but actually it's syntactic sugar for this:

f: WholeModel {-None,+a} -> WholeModel {-Any,+a}
= fn x => x;  # type error, identity function can't be given this type``````

Ugly Type Signatures

Algebraic Subtyping does not have type constraints as such, instead, it uses `&` and `|` constructions with type variables. This can lead to ugly type signatures:

``````# Pinafore (without type constraints)
predicate.SetModel : WholeModel {-((Entity & a) -> Boolean),+(a -> Boolean.)} -> SetModel (Entity & a)

# but if Pinafore had type constraints...
predicate.SetModel : (a <: Entity) => WholeModel (a -> Boolean) -> SetModel a``````

Pinafore doesn’t do this (yet), but you can mitigate this by allowing explicit constraints in type signatures, and rewrite them as needed. It’s even possible to extract constraints from types, in cases when you want to present inferred types to the user.

Function Purity

Like the Haskell it is implemented in, Pinafore separates “pure” functions from effects, using a monad (`Action`). As a Haskell developer, I happen to like this, and actually don’t find it awkward. But if you choose not to do this, and allow your functions to have side-effects, you may run in to various type-system gotchas, such as polymorphic references.

Algebraic Subtyping does not provide a way of overloading, for example, numerical functions on different types. For example, given two numeric types `Integer` and `Rational`, we should have negation functions for each:

``````negate: Integer -> Integer

negate: Rational -> Rational``````

However, even if we have the subtype relation `Integer <: Rational`, there is no clean way to combine these into one function. Pinafore does not solve this problem: it avoids it by simply having two functions with different names (`negate.Integer` and `negate.Rational`). This is made slightly easier with the use of namespaces.

If you really really wanted to, and I don’t at all recommend this, the best you can do is to create a special type and use conversions to do the actual negations. In Pinafore this terrible idea could be coded like this:

``````datatype Negate +a of Mk a end;
negate: a -> Negate a = Mk.Negate;
subtype Negate Integer <: Integer = fn Mk.Negate x => negate.Integer x;
subtype trustme Negate Rational <: Rational = fn Mk.Negate x => negate.Rational x;``````

Here the `+a` indicates that the type parameter is covariant. So this means you have `Negate Integer <: Negate Rational`.

So now you have a subtype “diamond”, that is, two separate subtype paths from the same types:

``````Negate Integer <: Integer <: Rational
Negate Integer <: Negate Rational <: Rational``````

If you don’t tell Pinafore `trustme`, it will reject the second subtype declaration, because it cannot prove that the paths work out to be the same (i.e., that the diamond “commutes”). But they are the same in this case, so it’s fine, and now you can use `negate` as if it were overloaded.

However, the whole approach requires a new type for each operation (`Negate` for `negate`, `Sum` for `+`, and so forth), and is ugly and counterintuitive for the user.

Representation

Whether to pick uniform or non-uniform representation will be your first major decision. Each of your language types will represented by some underlying “implementation type”, and each of your subtype relations will be represented by a conversion function on those implementation types.

With uniform representation, there is only one implementation type, and all conversion functions are represented by the identity function on that type. This will make your language implementation work much easier, as you will not have to keep track of conversion functions at all.

Non-Uniform Representation

Pinafore uses non-uniform representation instead. Doing this is a huge amount of work, as conversion functions need to be tracked everywhere, including through unification, subsumption, inversion, simplification, subtype picking, and anything else. You also need to keep track of the “functor maps” of each type variable of each ground type constructor, that is, how to convert `a -> b` to `F a -> F b`, etc.

The advantage of non-uniform representation is that it makes the language much more flexible. For example, in Pinafore it’s possible to define a subtype relation between two types already in scope by specifying the (pure) conversion function. If you want to take this route, you will almost certainly want to use Haskell, and you will probably end up basically replicating everything I did.

Some hints:

Meet & Join

Meet and join types can be represented in the obvious way, as product and sum data-types. Likewise, `None` and `Any` are represented as empty and unit types.

Conversions

Representing conversions as simple functions leads to unacceptable performance problems, as even small programs in your language will spend huge amounts of time running functions that convert between representations of trivially-equivalent types, such as `T | None``T``T & Any`. I solved this in Pinafore by replacing conversion functions with a conversion type, from which functions are derived. In this conversion type, certain trivial conversions have specific representation, so composition within the type can make the appropriate simplifications.

Type Variables

In Pinafore, type variables are represented by Haskell’s empty closed type families, and assignment of type variables is done using `unsafeCoerce`. This works provided a given type variable is never assigned more than once for each solving, and while I couldn’t statically guarantee this, I tried to make the code around these assignments as clear and specific as possible to be as confident as I could from code examination and testing.

Non-Equivalence

Representations of equivalent language types are not necessarily isomorphic as implementation types. For example:

``````x: Action (P | Q)

y: Action P | Action Q = x``````

There’s no implementation conversion from `Action (P | Q)` to `Action P | Action Q`, even though these are equivalent language types. Pinafore solves this essentially by cheating: when it comes across the type signature `Action P | Action Q`, it cheekily simplifies it to `Action (P | Q)` — since this is an equivalent type in Pinafore, the user will never know the difference.

Subtype System

The system of subtypes at any given scope must be consistent. This means:

• Given any type `A`, then `A <: A` and the subtype conversion `iAA` is identity.
• Given any types `A`, `B`, `C`, with `A <: B` and `B <: C`, then `A <: C` and the subtype conversions compose as `iAC = iBC . iAB` .

The important thing to remember is that there must be at most one subtype conversion function for any pair of types. Subtype “diamonds” (two different subtype paths between the same types) are allowed, but they must commute.

To make this work, you should ensure that there can be at most one subtype relation between any two ground type constructors. Here’s what happens if you violate this rule:

``````subtype Maybe Integer <: P = s1;
subtype Maybe Text <: P = s2;  # Pinafore will reject this line
g: P -> Unit = fn _ => ();

f = fn x => g (Just x);``````

What type can be inferred for `f`? Unification requires the subtype constraint `Maybe v <: P` to be solved, and only one of the two available conversions can be picked. Trying to pick both can only yield the non-type `Maybe (Integer | Text) -> Unit`, disallowed because `|` appears in negative position.

On the other hand, subtype relations with type variables (e.g. `F a <: G a`) are possible.

Record Types

The Algebraic Subtyping paper includes record types. I was hoping that record types could be used for functions with named parameters with defaults. But this doesn’t seem to work. Consider this:

``````# given this function
writeHandle: Handle -> Text -> Action Unit;

# define a function with named parameters, one with a default
write = fn {text: Text; handle: Handle = stdout;} => writeHandle handle text;

# some uses...
w1 = write {text = "hello";};
w2 = fn h => write {text = "hello"; handle = h;};
w3 = w2 stdout;  # OK
w4 = w2 3;  # oh no!``````

What type should be inferred for `write`? For `w1` to be accepted, it must be `{text:Text;} -> Action Unit`, but this means `w2` has type `Any -> Action Unit`, and the obviously unsound `w4` would be accepted.

Pinafore lets you define your own data types, and I couldn’t think of any other use for record types, so I omitted them from the language. But it might be possible to get optional parameters working by fiddling around with the nature of record types.

Recursive Types

Necessity

Recursive types are awkward to work with, and probably won’t have much use in your user’s programs, so you might wonder if you can omit them? In this case your solver would instead give a type error whenever the algorithm calls for a recursive type.

This might be possible given certain restrictions on subtype relations, but I don’t know the details. It’s certainly not possible for more general subtype relations, without sacrificing principality. Pinafore, for example, has the subtype relation `Maybe Entity <: Entity`, which means that the expression `let x = Just x in x` can have the types `Entity`, `Maybe Entity`, `Maybe (Maybe Entity)`, etc., but the principal type `rec a, Maybe a` must be recursive.

Understanding

In general I found it helpful to understand a given recursive type in three different ways:

• Using “mu” (or `rec` in Pinafore): `rec a, Maybe a`
• As a “let”-substitution (note this is not Pinafore syntax for types): `let a = Maybe a in a`
• Expanded: `Maybe (Maybe (Maybe (...`

It’s particularly helpful to keeping in mind the third, as it reinforces the fact that this type does not actually have any type variables. Of course it can’t be fully written out, and something like `rec a, (List a | Maybe a)` is even less “writable”.

The let-subst form represents the type as a context-free grammar, where each recursive variable is a nonterminal symbol. This type grammar is transformed during type simplification (see below).

Not Understanding

A couple of misunderstandings about recursive types that cost me effort:

• That `rec a, (P a | Q a)` is equivalent to `(rec a, P a) | (rec a, Q a)`. In fact it is not.
• That `rec a, a` can be rounded off to `Any` or `None`. It cannot. This “unguarded” syntax simply isn’t a type, and you must reject it if the user specifies it, since your algorithm will have it unify with every type. Your recursive types must follow both syntax restrictions mentioned in section 5.1.

Type Solving

Algorithms

There are currently two algorithms for solving types for unification and subsumption: Dolan’s original, and Lionel Parreaux’s Simple-sub. If you are using non-uniform representation, you must use Simple-sub, as there is a step in the Dolan algorithm that cannot be done while preserving the evidence you need (specifically, in section 5.3.3, in `biunify` branch “ATOM”, the substitution cannot be performed on the set of already-seen constraints).

If you are using uniform representation, you should probably use Simple-sub anyway. My guess is that it’s at least as fast, and it’s certainly much easier to understand.

Type Simplification

Both algorithms involve keeping a list of already-seen constraints to handle recursion, and between steps you must simplify the types to ensure your solver terminates. You will also want to simplify if you ever present inferred types to the user, for example, Pinafore has an “interactive mode” where it can show inferred types of expressions.

Pinafore does these simplifications in this order:

1. Simplify recursive types using grammars (see next section).
• `rec a, Maybe (rec b, a | Maybe b)``rec a, Maybe a`
2. Eliminate type variables that are “fully constrained”. This also includes “one-sided” type variables that only appear in positive position, or only appear in negative position.
• `(a & Integer) -> (a | Rational)``Integer -> Rational`
3. `None` and `Any` act as identities for `|` and `&`, respectively.
• `Integer | None``Integer`
4. Eliminate subtypes in joins:
• `Integer | Rational``Rational`
• `Integer & Rational``Integer`
5. Collapse matching parameterised types along their parameters:
• `List A | List B``List (A | B)`
• `(A -> X) | (B -> Y)``(A & B) -> (X | Y)`
6. Merge type variables that appear in all the same positive positions (or all the same negative positions):
• `a -> b -> (a | b)``a -> a -> a`
7. Roll up recursive types
• `Maybe (rec a, Maybe a)``rec a, Maybe a`

Type Grammars

Type grammars are necessary to simplify complex recursive types. For example, `rec a, Maybe (rec b, a | Maybe b)` is equivalent to `rec a, Maybe a`, although it isn’t obvious how to make this transformation.

To understand type grammars, consider how a type such as `rec a, (F a a | G a)` unrolls. It becomes an infinite tree with “left” and “right” branches at each `|`, and then branching for each type variable of `F` and `G`. You can think of this tree as a language on an alphabet of directions to move down the tree, and each path as a string in this language. A type grammar is simply the context-free grammar of this language.

To obtain a grammar from a type, we convert each use of `rec` into a production rule (renaming any duplicate variables). You can think of it as a kind of `let` form for types. For example, `rec a, Maybe. (rec b, a | Maybe b)` would be transformed to this:

``````let
a = Maybe (a | Maybe b)
b = a | Maybe b
in a``````

The simplification algorithm progressively unrolls the type by substituting production rules and merging branches (e.g. `Maybe P | Maybe Q` to `Maybe (P | Q)`). As it unrolls, it keeps track of the types it has seen, and when it comes across one it’s seen before, it emits a new use of `rec` at that point.

``````rec a, Maybe (rec b, a | Maybe b)

let
a = Maybe (a | Maybe b)
b = a | Maybe b
in a

RUN (a)
[substitute a]
RUN (Maybe (a | Maybe b))
[constructor]
Maybe (RUN (a | Maybe b))
[substitute a]
Maybe (RUN (Maybe (a | Maybe b) | Maybe b))
[merge]
Maybe (RUN (Maybe (a | Maybe b | b)) )
[constructor]
Maybe (Maybe (RUN (a | Maybe b | b) ))
[substitute a, b]
Maybe (Maybe (RUN (Maybe (a | Maybe b) | Maybe b | a | Maybe b) ))
[merge]
Maybe (Maybe (RUN (a | Maybe (a | Maybe b | b)) ))
[substitute a]
Maybe (Maybe (RUN (Maybe (a | Maybe b) | Maybe (a | Maybe b | b)) ))
[merge]
Maybe (Maybe (RUN (Maybe (a | Maybe b | a | Maybe b | b)) ))
[constructor]
Maybe (Maybe (Maybe (RUN (a | Maybe b | a | Maybe b | b)) ))
[merge]
Maybe (Maybe (Maybe (RUN (a | Maybe b | b)) ))
[already seen "RUN (a | Maybe b | b)"]
Maybe (Maybe (rec r, Maybe r))

(eventually rolled up to "rec r, Maybe r")``````

Type Inversion

If you allow type signatures, then you will do subsumption. But if you allow type signatures under a lambda, you must also do type inversion. Here’s an example, given some positive type `T`:

``````fn x => let
y: T = x
in y``````

What is the type of this expression? Well, it’s `T -> T`, with `T` now also in negative position. When is this permissible?

Given a positive type `T+`, there is some set of positive types `S(T+)` that subsume to `T+`. The inversion `T-`, if it exists, is the type such that the set of positive types `U(T-)` that unify with `T-` is the same as `S(T+)`.

As a rule of thumb, a type is invertible if (after simplification) it has no type variables or use of `&`, `|`, `Any`, or `None`.

Going Further

Parreaux and the team at HKUST have a more powerful type system implemented in their MLscript language, allowing union and intersection without regard to type polarity, as well as type negation. I don’t know how amenable it is to non-uniform representation.

— Ashley Yakeley

Pinafore 0.5

A much smaller update, this time.

``````  * Language
- redesign dynamic types
- allow decarations in do-blocks
* Library
- built-in
. improve type of getList.FiniteSetModel
- GTK
- UILib
. update``````

The main improvement is a reworking of dynamic types. Before, they had to be defined bottom up, that is, you had to define the concrete types first, and then define abstract supertypes in terms of them.

``````# old Pinafore
dynamictype Human = !"Human";
dynamictype Cat = !"Cat";
dynamictype Dog = !"Dog";
dynamictype Animal = Human | Cat | Dog;``````

Now, however, you can define the types in any order, and then simply declare subtype relations:

``````# new Pinafore
dynamictype Animal;
dynamictype Human = !"Human";
subtype Human <: Animal;
dynamictype Cat = !"Cat";
subtype Cat <: Animal;
dynamictype Dog = !"Dog";
subtype Dog <: Animal;``````

This is much more flexible, and matches the way open entity types work. The only caveat is that the behaviour of abstract dynamic types (e.g. `check @Animal`) varies depending on what subtype relations are in scope.

— Ashley Yakeley

Pinafore is an interpreted purely functional language using Algebraic Subtyping that explores structuring information and composing graphical user interfaces.

It has a number of unusual features, some fairly trivial, some more significant, some occasionally found in other programming languages, and some I believe are entirely unique to the language.

As an interpreted language written in Haskell, Pinafore programs use the Haskell run-time system. In addition, Pinafore borrows a lot of features from Haskell. As a baseline, if a feature is also part of Haskell, I don’t count it as an Unusual Thing. These include, for example:

• A type system that extends Hindley-Milner
• Type inference
• User-defined data types with constructors
• Constructor pattern matching
• Separation of pure functions from effects
• Laziness
• Garbage collection

Pinafore’s syntax is somewhat different. Here’s a quick cheat-sheet of equivalent Haskell and Pinafore syntax and types:

1. Algebraic Subtyping

Algebraic Subtyping is a fairly recent type system that extends Hindley-Milner with subtyping in a way that is decidable and has principality. To achieve this, it distinguishes positive and negative types, and makes use of union and intersection types.

As far as I know, Pinafore is the only non-academic implementation of Algebraic Subtyping.

Why did I pick this type system? Part of the purpose of Pinafore is to represent information in an intuitive manner, and people naturally think in terms of subtypes, e.g. “every dog is an animal”, “every apple is a fruit” and so forth. And Hindley-Milner-based approaches are much cleaner mathematically, and therefore easier to reason about, than the kind of two-level type systems you find in languages such as Java, C#, C++ and so forth.

A subtype relation between types `P` and `Q`, written `P <: Q`, and pronounced “`P` is a subtype of `Q`“, simply means “every `P` is a `Q`“, or “accept a `P` where a `Q` is expected”. It implies a conversion function from `P` to `Q`. As an example, Pinafore has three numeric types `Integer`, `Rational`, and `Number`, with the intuitive subtype relations `Integer <: Rational <: Number`. So you can pass an `Integer` to a function expecting a `Rational`, and Pinafore will perform the conversion implicitly.

It’s important to note that in this type system, and in Pinafore, conversion functions do not need to be injective, nor does a retraction function `Q -> Maybe P` need to exist. It’s perfectly OK for type conversion to lose information. The only constraint is that, at any given point in your program, the system of subtype relations that are in scope must be consistent. This essentially means that “subtype diagrams commute”, that is, if there is more than one subtype “path” for the same types, it must imply the same conversion function.

Algebraic Subtyping, like Hindley-Milner, has type variables, and types can be constructed from type constructors that have parameters. In Algebraic Subtyping, however, each type parameter of each type constructor must be either covariant or contravariant. In cases such as a “reference cell” for which the type parameter would not naturally be either, a contravariant/covariant pair of type parameters is used instead. Pinafore has a special syntax for such pairs to make them easier to work with. The “optics” section of the library makes particular use of these, corresponding to similar pairs of parameters in various optics types in Haskell and Scala.

Algebraic subtyping can give types to expressions that Hindley-Milner cannot. For example:

``````pinafore> :type fn x => x x
: (a -> b & a) -> b
pinafore> :type fn f => (fn x => f (x x)) (fn x => f (x x))
: (a -> a) -> a``````

Pinafore’s implementation of Algebraic Subtyping includes equirecursive types, which are necessary as the principal types of certain expressions. They are, however, not particularly used. Pinafore omits the record types defined in the paper.

A quick note on terminology, for those familiar with this type system: a positive type is a type that can appear in positive position, likewise a negative type, while an ambipolar type is one that is both positive and negative, and a concrete type is a type with no free type variables.

2. General Subtype Relations

Given two types `P` and `Q` already in scope, Pinafore lets you declare a subtype relation `P <: Q` simply by providing the conversion function of type `P -> Q`.

As far as I know, there is no other programming language that implements this.

Here’s an example, defining a subtype relation from `Map a` to the function type `Entity -> Maybe a`:

``````subtype Map a <: Entity -> Maybe a =
fn m, e => lookup.Map e m;``````

The `Map` type and function type are already defined, and here we declare a subtype relation. So now we can treat maps as functions.

Of course, since Pinafore separates pure functions from effects, these conversion functions are all pure functions without effects.

To maintain consistency, Pinafore will reject any subtype declaration if it would create a subtype “diamond” (two different subtype paths from the same types), since it cannot prove that the diamond commutes. But if you want to override this, because you want Pinafore to blindly accept your claim that the two paths are the same conversion, then you can add the `trustme` flag to the declaration.

3. Greatest Dynamic Supertype

Subtype conversion functions do not need to have retractions. But, some of them do! Pinafore provides a general mechanism for working with them, the greatest dynamic supertype.

Here’s how it works. Every (concrete ambipolar) type `T` has a greatest dynamic supertype `D(T)`, with these properties:

• `T <: D(T)`supertype
• `D(D(T)) = D(T)`greatest
• The retraction function is defined: `check @T: D(T) -> Maybe T`dynamic

(Note that `check` is a “special form” that requires specifying a type, rather than an ordinary binding.)

So for most `T`, `D(T) = T`, which is not very interesting. However, for example, the GDS of all literal types (numeric types, `Text`, date & time types, etc.) is `Literal`, which internally stores (“dynamically”) the run-time type. So if you have `Literal`, you can inspect it with `check @Rational` to obtain the `Rational` if it represents one.

Alternatively, there’s a pattern-matching form `:?` that does the same thing as `check`:

``````match
t :? Rational => Just t;
_ => Nothing
end``````

If you define a subtype within a datatype definition, then that will give the appropriate GDS relationship:

``````let rec

datatype List +a of
Nil;
subtype datatype List1 of
Cons a (List a);
end;
end;

end;``````

This defines two type constructors, `List` (representing lists), and `List1` (representing non-empty lists), both of which have one covariant parameter, with `List1 a <: List a`, and `D(List1 a) = List a`.

4. No Top Level

A main program is an expression. All declarations, including name bindings, type declarations, and subtype relation declarations, are within `let` or `let rec` declarators.

It’s perfectly OK for values to escape the scope of their types. They typically can’t be used at that point, but I don’t believe that that’s unsound. Internally, each type is assigned an ID, so there’s no possibility of aliasing a different type with the same name.

5. “Backwards” Name Qualification

Name qualification in Pinafore runs in the order specific-to-general. For example, the name `a` within namespace `N` within namespace `M` is referred to, fully qualified, as `a.N.M.` (note dot at end). This is the reverse of how it’s done in most other languages such as C++ (which would have `::M::N::a`) or Java (`M.N.a`).

So why? It’s simply easier to read, especially as the capitalisation of the first letter of the name is significant. Note that the data constructors of a type are placed in the “companion namespace” of the type, and this too is easier to read with this order.

Pinafore does not have anything like Haskell’s type classes, and there is no overloading, so namespaces play a bigger role in distinguishing equivalent functions for different types.

``````datatype Expression +a of
Closed a;
Open Text (Expression (Value -> a));
end;

evaluate: Expression a -> Action a =
match
Closed.Expression a => pure.Action a;
Open.Expression name _ => fail \$ "undefined: " <>.Text name;
end;``````

Perhaps this is a matter of taste, but I find `Open.Expression`, `pure.Action`, and `<>.Text` to be easier to read than `Expression.Open`, `Action.pure`, and `Text.<>`.

6. Record Constructors

Data type definitions look like this:

``````datatype D of
Mk1 T1 T2 T3;
Mk2 T4;
end;``````

`Mk1.D`, `Mk2.D`, etc. are data constructors, and `T1`, `T2`, etc. are types. These types must be concrete (i.e. monomorphic, no free type variables), and ambipolar.

Why is this? Consider the types of these expressions:

``````Mk2.D: T4 -> D

fn Mk2.D t => t: D -> T4``````

As you can see, `T4` appears in both negative and positive positions, and these are the only ways to use the `Mk2.D` constructor to construct and examine values of `D`.

Record constructors are a different kind of constructor, that allow you to store any polymorphic positive types. They look like this:

``````datatype Record of
Mk of
f: (a -> a) -> a -> a;
g: Integer;
h: Action a -> Action (Action a);
end;
end;``````

`Mk.Record` is a record constructor, and when matched as a pattern, it brings its members `f`, `g`, `h` into scope.

``fn Mk.Record => f: Record -> (a -> a) -> a -> a``

To use it to construct a `Record`, you can do this:

``````Mk.Record of
f = fn x, a => x (x a);
g = 17;
h = map.Action pure;
end``````

7. Expose Declarations

Pinafore gives you fine-grained control of which names to expose out of a declaration. Here’s an example:

``````let
a = 1;

let
p = 2;
q = 7;
r = p * q;
in expose p, r;

in a + p + r``````

The expose-declaration (`let``in expose p, r`) exposes `p` and `r`, but not `q`, within the bindings of the outside `let`– expression.

This sort of thing is useful for creating “subset” and “quotient” types of a given type. For example, consider the `Text` type, for representing strings of text. Lower-case text is a subset of text, where only some text (all lower case) can be constructed. Case-insensitive text is a quotient of text, where text-case cannot be distinguished. We can create Pinafore for both of these types by carefully exposing certain functions and hiding others:

``````let

datatype LowerCaseText of Mk Text end;
subtype LowerCaseText <: Text = fn Mk.LowerCaseText t => t;

datatype InsensitiveText of Mk Text end;
subtype Text <: InsensitiveText = Mk.InsensitiveText;

myToLowerCase: InsensitiveText -> LowerCaseText =
fn Mk.InsensitiveText t => Mk.LowerCaseText \$ toLowerCase t;

in expose LowerCaseText, InsensitiveText, myToLowerCase;``````

Note that the two types we have defined are exposed, but not their data constructors. (Subtype relations are always exposed.) Thus, we can examine a value of type `LowerCaseText`, since it’s a subtype of `Text`, but we can’t create one except with our `myToLowerCase` function. Likewise, we can create a value of type `InsensitiveText`, since it’s a supertype of `Text`, but we can’t examine it except with our `myToLowerCase` function.

8. Soft Exceptions

``````stop: Action None;

onStop: Action a -> Action a -> Action a;``````

In Pinafore, any action can stop. For example, attempting to change a model that happens to be immutable will stop. Trying to retrieve missing/null data will stop. Or you can just call `stop`. This is essentially a kind of exception, which can be caught, if you want, with `onStop`.

Stops are “soft” in the sense that they are intended to control flow rather than indicate an error or exceptional condition. Default handlers (e.g. for button presses, or the main program) will catch and silently discard the stop without raising any kind of further error or complaint. The idea is, the user clicks the button or whatever, and if the action fails, by default nothing else happens.

As such, `stop` can be used much like `break` in C, for breaking out of iteration rather than indicating a problem. For example:

``````tryStop_ \$ forever \$ do
m >- match
Item.ItemOrEnd x => someaction x;
End.ItemOrEnd => stop;
end;
end;``````

9. Live Models

The purpose of Pinafore is to represent information, and compose user interfaces (using GTK) for it. If you’re familiar with the “model/view/controller” approach to user interface, Pinafore separates “models” of various types from “view/controller”. These combine to make a UI element (GTK widget) that can be laid out in a window.

A model represents some information than can change and be changed. It might be a file, or information in storage (see below), or simply pure memory. Change goes in both directions: the UI “controller” can change the model in response to user input (by calling functions on it), and the model can change the UI “view” (the UI subscribes to updates from the model). Multiple widgets can be constructed from the same model, or from composed models; and changes from one widget will cause asynchronous updates to other widgets, to keep them all consistent.

It is not enough to represent the type of some piece of information, one must also represent the characteristic ways that that information changes. For example, something simple like a flag or a number changes as a whole, that is, the entire value is replaced. But something like a list or a set or text changes in a more complicated manner, with, for example, insertions and deletions. To represent changeable information properly, the various types of changes must be represented.

Pinafore has a number of model types to represent changeable information, each with its own type for changes and updates. The simplest is `WholeModel T` for any given type `T`. This simply represents information of type `T` that can be retrieved, set and updated as a whole value, with no further structure. Values of `WholeModel` can be composed in various ways, including applicatively (see below).

By contrast, `ListModel T` represents a list of elements each of type `T`, where individual elements can be retrieved, inserted, deleted, and changed. The type of updates from the model to the UI specifies insertion/deletion/change, so the UI view can react cleanly to the semantic of the update. You can also pick out an element of a `ListModel T` to get a `WholeModel T`, which will track that element as other elements are inserted and deleted around it.

A `TextModel` tracks insertions/deletions/replacements of text. A `SetModel T` tracks additions and deletions of members of type `T`. A `FiniteSetModel T` is a `SetModel T` that also tracks its list of members. It is possible to compose some of these model types in various set-theoretic ways (unions, intersections, Cartesian sums and products).

10. Declarative User Interface

Pinafore uses GTK to provide user interface, however, all UI elements (“widgets”) are created declaratively by connecting them to models. Thereafter, changes to the UI reflect changes to the models.

``````open.Window gtk (300,400) {"My Window"} \$ vertical.Widget
[
horizontal.Widget
[
button.Widget {"<"} {do d <- get r; r := pred.Date d; end},
layoutGrow.Widget \$ label.Widget {encode (unixAsText.Date "%A, %B %e, %Y") %r},
button.Widget {">"} {do d <- get r; r := succ.Date d; end}
],
layoutGrow.Widget \$ textArea.Widget (fromWhole.TextModel \$ dateNotesOf !\$ r)
];``````

In this example, the widgets are simply declared in a static structure, and don’t need to be referred to again. Any aspect of a widget that can change is connected to a model: when the model updates, the widget will change. When the user interacts with the widget, it will pass those changes to the model.

But what if some part of the widget structure itself should change dynamically, in response to user actions? For that there’s the dynamic widget:

``dynamic.Widget: WholeModel +Widget -> Widget``

Simply create a whole-model of how the widget structure should change in response to other models, and pass it to `dynamic.Widget` as your widget.

11. Declarative Drawing

Pinafore provides bindings to Cairo for drawing functions, which can be used to construct your own GTK UI widgets. Rather than using an imperative style as Cairo usually provides, Pinafore’s Cairo bindings are declarative: the basic Cairo type is `Drawing`, and visual elements of type `Drawing` can be appropriately composed and modified, without having to work with any kind of mutable context state.

Here’s a complete Pinafore program that creates a window with a rotating red triangle on top of a navy disc:

``````import "pinafore-gnome", "pinafore-media" in
with GTK., Cairo., Drawing.Cairo., Number. in
let
pointer: Drawing None =
with Path., Colour. in
source red \$ fill \$ concat [moveTo (-0.1,0), lineTo (0.1,0), lineTo (0,1), close];

disc: Drawing None =
with Path., Colour. in
source navy \$ fill \$ arc (0,0) 1 0 (2*pi);
in
newClock (Seconds 0.1) >>= fn now =>
run.GTK \$ fn gtk =>
open.Window gtk (400,400) {"Drawing"} \$
draw.Widget
{
fn (w,h) =>
let angle = %now >- fn SinceUnixEpoch (Seconds ss) => ss / 10 in
translate (w/2,h/2) \$ scale (w/2,h/2) \$ concat [disc, rotate angle pointer]
}``````

You can see the drawing code in the following lines. This creates a closed triangular path, and fills it with red:

``source red \$ fill \$ concat [moveTo (-0.1,0), lineTo (0.1,0), lineTo (0,1), close]``

This creates a complete circle and fills it with navy:

``source navy \$ fill \$ arc (0,0) 1 0 (2*pi)``

This layers the rotated pointer over the disc, and scales and translates it to the window’s co-ordinate system:

``translate (w/2,h/2) \$ scale (w/2,h/2) \$ concat [disc, rotate angle pointer]``

Since the drawing is converted to a GTK widget, one can also add click actions for particular drawing elements.

12. Lifecycles

Many actions require some later “closing” or “clean-up”, for example, opening a GUI window means it will be closed again, or starting an asynchronous task means waiting for it to complete, and so forth. These are sometimes called resources.

Pinafore has a general mechanism for working with resources, called lifecycles. The basic idea is that any resource “opened” in a lifecycle will be “closed” at the end of that lifecycle.

These are the functions provided:

``````run.Lifecycle: Action a -> Action a;

onClose.Lifecycle: Action Unit -> Action Unit;

closer.Lifecycle: Action a -> Action (a *: Action Unit);``````

Calling `run` on an action will run it in a new lifecycle. Thus, if a GUI window is opened in that action, it will be closed at the end of the `run` call.

Calling `onClose` will create a “closing action” for your own resource. Closing actions will be run (in reverse order of creation) at the end of the lifecycle.

Calling `closer` on some action that opens resources gives the result of that action together with its (idempotent) “closer”. Calling the closer allows you to close the resources at any time, before the end of the lifecycle, allowing closing of resources in any order.

A Pinafore program is itself run in a lifecycle, that will run closers before exiting, so all resources will be cleaned up.

13. Applicative Notation

Pinafore does not have type classes, and all type variables have kind `*`, so there is no equivalent to Haskell’s `Applicative` class. Nevertheless, certain type constructors are essentially applicative, and Pinafore has a special notation for composing them applicatively. These include `Action`, `Maybe`, `Task` (see below), `List`, `WholeModel`, among others, though you can define your own, if you define the correct functions in a namespace.

``````pinafore> {.List %[3,4,5] + %[10,20]}
[13, 23, 14, 24, 15, 25]``````

In this example, two lists are combined applicatively. The braces `{ .. }` indicate applicative notation, and `.List` is the namespace from which applicative operations `pure`, `map`, `ap`, etc. are obtained. This is how it gets converted:

``````{.List %[3,4,5] + %[10,20]}

ap.List (ap.List (pure.List (fn var1, var2 => var1 + var2)) [3,4,5]) [10,20]``````

Applicative notation is particularly useful for working with whole-models. Models created in this way are immutable, however, their updates are propagated. The `WholeModel` namespace is the default for applicative notation if the namespace is omitted.

``````import "pinafore-gnome" in
run.GTK \$ fn gtk =>
do
now <- newClock \$ Seconds 1;
open.Window.GTK gtk (400,400) {"Clock"} \$
label.Widget.GTK {"The time is " <>.Text show %now};
end``````

In this example, `now` is a model of a clock that updates every second with the current time. It has type `WholeModel +Time`. The notation `{"The time is " <>.Text show %now}` of type `WholeModel +Text` creates a model of text that updates every second. Running this program will create a window with a label widget with text that updates every second.

Note that the title of the window, `{"Clock"}`, is also a whole-model, although in this case of constant text.

Pinafore uses a locking system to make GTK user interface code thread-safe. When a live model (see above) updates, subscriptions to that update happen in a new thread, which may call GTK. Functions to set and change models are also atomic and thread-safe.

As part of this design, Pinafore makes wide use of threads rather than relying on the kind of yielding state machines found in C#. A task in Pinafore is simply anything that can be waited upon for completion with a result value.

``````async.Task: Action a -> Action (Task a)

Pinafore does have a function `async`, but in this design it simply starts a task running in a new thread. Tasks started in this way complete in the current lifecycle, that is, calling `async` creates a lifecycle-closing action that waits for the thread to complete.

Tasks can be composed applicatively using `pure`, `map`, `**`, etc., or using applicative notation. Waiting on such a task simply waits for all its component tasks to complete, and then combines the result values.

15. Robust Storable Data

Pinafore has a built-in storage system, storing data in a SQLite file in a directory in your home directory.

Pinafore storage is designed to be robust with regards to changes in data schema. New constructors can be added to storable data types without affecting existing data in storage. Constructors can also be removed: such data is simply considered null or missing, and the usual retrieval function will “stop” (see above).

Only certain types are storable. But Pinafore does not store values of types as such. You cannot, for example, retrieve all values of a type. Rather, Pinafore stores subject-property-object triples. The subject and object of each triple are values of storable types. Properties are declared in code. You can retrieve the object of a given subject and property. You can also retrieve the set of subjects for a given property and object. Pinafore stores knowledge rather than items.

``````let
opentype Person;
name: Property Person Text = property @Person @Text !"person-name" store;
dave: Person = point.OpenEntity @Person !"my friend dave";
in name !\$ {dave} := "Dave"``````

In this example, `opentype Person` creates a new open entity type. Open entity types are purely abstract points: they are represented and stored as 256 random or hashed bits and have no further internal structure or meaning. Instead, they are used as subjects and objects of properties.

In the next line, `property @Person @Text !"person-name" store` defines a `Text` property of `Person`. Triples with this property will have a subject of type `Person` and an object of type `Text`. `!"person-name"` is an anchor, which is hashed and used to identify the property in storage. The binding `property` is a “special form”: something that takes (constant) type and anchor arguments. (The `store` argument represent storage, obtained from `openDefault.Store`.)

Properties can be composed and combined in various ways: for example, `name ..Property father` is a property for “father’s name”, while `name **.Property father` is a property for “name and father”.

The special form `point.OpenEntity` defines fixed values of open entity types, in this case a value of type `Person` identified in storage by the given anchor. Points can also be generated randomly.

The last line `name !\$ {dave} := "Dave"` constructs a model, `name !\$ {dave}`, and then sets it to the text. This model can also be passed to a user interface widget, which would be able to set it, and also be automatically updated when it changes.

Properties can also be used “in reverse”, for example, `name !@ {"Dave"}` will retrieve a `FiniteSetModel` of all points in storage with `name` set to `"Dave"`.

You can create your own polymorphic storable data-types, however all types mentioned in constructors must be storable, and all type parameters must be covariant. Each constructor is given an anchor to identify it in storage. For example:

``````let rec
datatype storable Tree +a of
Mk a (List (Tree a)) !"Mk.Tree";
end;
end;``````

Since open entity types represent abstract points without further structure, subtype relationships between them can be declared arbitrarily without providing any conversion functions, or worrying about “diamonds”. For example:

``````opentype Named;
name = property @Named @Text !"name" store;

opentype Living;
birthdate = property @Living @Date !"birthdate" store;
deathdate = property @Living @Date !"deathdate" store;

opentype Person;
subtype Person <: Named;
subtype Person <: Living;``````

And since open entity types represent simple points, they don’t carry type information. For example, if you have an value of type `Living`, you cannot determine whether or not it is a `Person`. To store type information, you can use dynamic entity types instead:

``````dynamictype Human = !"Human";
dynamictype Cat = !"Cat";
dynamictype Mammal = Human | Cat;
dynamictype Bird = !"Bird";
dynamictype Animal = Mammal | Bird;``````

Like open entity types, dynamic entity types are storable, but each value internally stores an anchor representing its “dynamic type” or “runtime type”. The greatest dynamic supertype of all dynamic entity types is `DynamicEntity`, so it’s easy to check a dynamic type at run-time:

``````checkMammal: Animal -> Maybe Mammal =
match
m :? Mammal => Just m;
_ => Nothing;
end;``````

16. Undo Handling

Being able to undo and redo actions is an essential part of user interface. Pinafore provides functions to create “undo handlers” and connect them to storage or to specific models. Changes to these things will be recorded to a queue, and can then be undone and redone.

``````new.UndoHandler: Action UndoHandler

handleStore.UndoHandler: UndoHandler -> Store -> Action Store
handleWholeModel.UndoHandler: UndoHandler -> WholeModel a -> WholeModel a
handleTextModel.UndoHandler : UndoHandler -> TextModel -> TextModel
# etc., for all model types

queueUndo.UndoHandler : UndoHandler -> Action Boolean
queueRedo.UndoHandler : UndoHandler -> Action Boolean``````

Future Directions

Everything above is available in the latest release of Pinafore, version 0.4.1. But I have lots more ideas and plans for future versions.

On the language side:

• Predicate types: types which need to satisfy a user-supplied predicate to construct. Thus you could create a “type of prime numbers”.
• Existential types: a record constructor could declare a type name, to be instantiated with a type when the value is constructed.

More general feature ideas:

• Graphs and charts, especially along the lines of The Grammar of Graphics.
• Easy connection to external data sources.
• More composability of user-interface widgets, such as variable lists and grids of a given widget type.

Pinafore 0.4.1 is available as a Debian package for 64-bit Linux, that will work on Ubuntu 22.04 (and derivatives), Debian 12, and later. There is also a Nix flake for 64-bit Linux. Go to pinafore.info.

— Ashley Yakeley

Pinafore 0.4

I’ve just released version 0.4 of Pinafore, representing more than a year’s worth of full-time work since the last release.

I’ll make another post shortly explaining what Pinafore is all about and what makes it unusual, but in the mean time, this is the release notes for the new version:

``````  * Install
- Debian package works on:
. Ubuntu 22.04 LTS "jammy"
. Debian 12 "bookworm"
* Language
- overhaul of declarations
. separate namespaces from modules,
with "namespace" declarations and "with" and "import" declarators
. both non-recursive ("let") and recursive ("let rec") declarators
. "expose" declarations
. allow declaration documentation with #| and {#| #} comments
- datatype declarations
. "closedtype" now "datatype storable"
. can now have parameters
. can now have subtypes
. record constructors/patterns for datatypes
. allow recursive types in datatypes
- can declare arbitrary subtype relations
- import lists
- syntax
. allow defintion of new operators
. changed recursive type syntax from "rec v. T" to "rec v, T"
. type names (+:), (*:), List, Unit
. tuple constructor/pattern (,,) etc.
. type signatures now attach to bindings, not stand-alone
. separate syntax for static ":" and dynamic ":?" pattern typing
. new syntax for function expressions: fn, match, =>
. new syntax for datatype definitions
. generalised "{}" and "do" syntax to any namespace
- reject rather than mutate uninvertible type signatures
- allow polymorphic recursion with type signatures
* Interactive
- :doc to retrieve name documentation
* Library
- Std
. Literal type now byte array rather than text
. Literal types now have GDS Literal
. add Showable type for showing, show replacing toText
. add List1 type for non-empty lists, subtype of List
. rename "Ref" types and functions to "Model"
. add TextModel type & associated functions, use for uiTextArea
- new Stream module
- new Env module
. move invocation-type stuff here
- new Eval module
. move evaluate here
- new Colour module
. add Colour & AlphaColour types, etc.
- new GIO module
. add GIO File type and functions
- new Cairo module
. add Cairo-based functions for creating drawings
- new Image module
- GTK
. rename (from "UI")
. explicit control over context
. menu bar is just ordinary element
. element for Image
* Storage
- Anchors now 256 bit, hash using BLAKE3
- Store literals as binary rather than as text
- Embed smaller literals directly in the anchor
* Fixes
- fix defect in lexical scoping
``````

— Ashley Yakeley

Monadology is intended as a collection of the best ideas in monad-related classes and types, with a focus on correctness and elegance, and theoretical understanding, rather than practical performance. I am interested in hearing further ideas, so at least initially expect a lot of change version-to-version.

Re-exported Transformers

Monadology is built on the existing transformers package. It re-exports most of it. (It does not re-export `ListT`).

Result

This general-purpose “result” monad represents either success or failure, of any type. This sort of thing is so useful it could have been in base, but it isn’t.

``````data Result e a
= SuccessResult a
| FailureResult e``````

Of course, it’s isomorphic to `Either`. But whereas `Either` has a more general-purpose “symmetrical” feel, `Result` is more intelligible to the reader as a monad.

Exceptions

Monadology makes two separate approaches to exceptions: one type and many types. For example, for the `IO` monad, there are many different exception types that can be both thrown and caught. But there is also the one type `SomeException` that represents all the possible exceptions.

Many Types

For the many-types approach, Monadology simply provides `MonadThrow` and `MonadCatch` classes, along with various functions:

``````class Monad m => MonadThrow e m where
throw :: forall a. e -> m a

catch :: forall a. m a -> (e -> m a) -> m a``````

One Type

In principle, every monad `m` has a single type of all the exceptions it can throw and catch. For this approach, this type is named `Exc m`:

``````class Monad m => MonadException m where
type Exc m :: Type
throwExc :: Exc m -> m a
catchExc :: m a -> (Exc m -> m a) -> m a

type Exc Identity = Void
type Exc ((->) r) = Void
type Exc Maybe = ()
type Exc (Result e) = e
type Exc (ExceptT e m) = Either e (Exc m)
type Exc (StateT s m) = Exc m
type Exc IO = SomeException``````

Functions such as `finally` and `bracket`, that make no reference to any particular exception type, make use of this to ensure that they work for all exceptions that can be thrown.

You can compose two functors to get a functor. And you can compose two applicative functors to get an applicative functor. But, famously, you cannot compose two monads to get a monad.

At least, you cannot in general. But you can, of course, in certain cases. And we can capture the most useful cases by specifying the constraints we need on one of the monads so as to leave the other unconstrained.

`MonadInner` is just the right constraint on the inner monad so as to compose with any outer monad to get a monad.

``````class (Traversable m, Monad m) => MonadInner m where
retrieveInner :: forall a. m a -> Result (m Void) a

newtype ComposeInner inner outer a = MkComposeInner (outer (inner a))

Essentially, `inner a` must be isomorphic to `Either P (Q,a)` for some `P`, `Q`. If you examine the structure of the `WriterT`, `ExceptT`, and `MaybeT` monad transformers, you’ll see that they are cases of this composition pattern.

`MonadOuter` is just the right constraint on the outer monad so as to compose with any inner monad to get a monad.

``````newtype WExtract m = MkWExtract (forall a. m a -> a)

getExtract :: m (WExtract m)

newtype ComposeOuter outer inner a = MkComposeOuter (outer (inner a))

Essentially, `outer a` must be isomorphic to `P -> a` for some `P`. If you examine the structure of the `ReaderT` monad transformer, you’ll see that it’s a case of this composition pattern.

Lifecycles

`LifecycleT` is a monad transformer for managing the closing of opened resources, such as file handles, database sessions, GUI windows, and the like. You can think of it as a conceptually simpler version of `ResourceT`.

The actual code is slightly different in the contents of the `MVar`, but it basically looks like this:

``````newtype LifecycleT m a = MkLifecycleT (MVar (IO ()) -> m a)

runLifecycle :: (MonadException m, MonadTunnelIO m) => LifecycleT m a -> m a

type Lifecycle = LifecycleT IO -- the most common usage``````

That `MVar` simply stores all the “close” operations to be run at the end of each “lifecycle” when called by `runLifecycle`, in reverse order of their opening. You can add your own close operations with `lifecycleOnClose`.

Of course you may be thinking, what if I want to close things in a different order? For example, GUI windows get closed when the close box is clicked, not in the reverse order of opening.

For this you want to get a closer function:

``lifecycleGetCloser :: MonadIO m => LifecycleT m a -> LifecycleT m (a, IO ())``

For example,

``````newGUIWindow :: Lifecycle Window

makeMyWindow :: Lifecycle Window
makeMyWindow = do
(window,closer) <- lifecycleGetCloser newGUIWindow
lift \$ onCloseBoxClicked window closer
return window``````

Here, `closer` is an idempotent operation that will call the closer of `newGUIWindow`, that is, to close the window. Subsequent calls do nothing. It also gets called at the end of the lifecycle, to ensure that the window is eventually closed if it hasn’t been already.

Also, you may come across certain functions that make use of the “with” pattern, to manage opening and closing. Here are a couple from the base library:

``````withFile :: FilePath -> IOMode -> (Handle -> IO r) -> IO r

withBinaryFile :: FilePath -> IOMode -> (Handle -> IO r) -> IO r``````

Monadology is capable of “unpicking” this pattern coroutine-style, and converting it to a `Lifecycle`:

``````lifecycleWith ::  (forall r. (a -> IO r) -> IO r) -> Lifecycle a

fileHandle :: FilePath -> IOMode -> Lifecycle Handle
fileHandle path mode = lifecycleWith \$ withFile path mode``````

Coroutines

Speaking of coroutines, Monadology has a class for that.

``````class Monad m => MonadCoroutine m where
coroutineSuspend :: ((p -> m q) -> m r) -> CoroutineT p q m r``````

This is experimental, as the only useful instances I’ve come across are monads based on `IO`, which supports coroutines by using threads.

The `CoroutineT` transformer is a special case of the `StepT` transformer, which is for step-by-step execution.

Transitive Constraints

For many transformers, certain constraints on a monad are transitive to the transformed monad. For example:

``````Monad m => Monad (ReaderT r m)

Monadology has a class for this:

``````class TransConstraint c t where
hasTransConstraint :: forall m. c m => Dict (c (t m))

instance Monoid w => TransConstraint MonadPlus (WriterT w)

Why not just use GHC’s `QuantifiedConstraints` extension? Because GHC has issues satisfying quantified constraints. So there’s an explicit class instead.

Tunnelling, Hoisting and Commuting

Tunnelling allows you to manipulate monads underneath a transformer. Each tunnellable transformer is associated with a tunnel monad, that represents the “effect” of the transformer.

``````type p --> q = forall a. p a -> q a

(m1 --> m2) -> t m1 --> t m2

type Tunnel t :: Type -> Type
tunnel :: forall m r. Monad m =>
((forall m1 a. Monad m1 => t m1 a -> m1 (Tunnel t a)) -> m (Tunnel t r)) -> t m r``````

Tunnel monads are, curiously enough, always instances of the aforementioned `MonadInner`. For example:

``````type Tunnel (ReaderT s) = Identity
type Tunnel (WriterT w) = (,) w
type Tunnel (StateT s) = (,) (Endo s)
type Tunnel MaybeT = Maybe
type Tunnel (ExceptT e) = Either e
type Tunnel (ComposeInner inner) = inner
type Tunnel (ComposeOuter outer) = Identity``````

(This is essentially a correction and generalisation of `MonadTransControl`.)

It’s straightforward to derive hoisting from tunnelling, which is why `MonadTransHoist` is a superclass of `MonadTransTunnel`. And furthermore, you can commute two transformers in a stack, if you can commute their tunnel monads (which you always can).

``````commuteTWith :: (MonadTransTunnel ta, MonadTransTunnel tb, Monad m) =>
(forall r. Tunnel tb (Tunnel ta r) -> Tunnel ta (Tunnel tb r)) ->
ta (tb m) --> tb (ta m)

commuteInner :: (MonadInner m, Applicative f) => m (f a) -> f (m a)

ta (tb m) --> tb (ta m)
commuteT = commuteTWith commuteInner``````

Unlifting

Monadology has two classes for unlifting transformers.

``````type Unlift c t = forall m. c m => t m --> m
newtype WUnlift c t = MkWUnlift (Unlift c t)

class (...) => MonadTransUnlift t where
-- | lift with an unlifting function that accounts for the transformer's effects (using MVars where necessary)
liftWithUnlift :: forall m r. MonadIO m =>
(Unlift MonadTunnelIOInner t -> m r) -> t m r
-- | return an unlifting function that discards the transformer's effects (such as state change or output)

-- | A transformer that has no effects (such as state change or output)

Only `ReaderT` (and `IdentityT`) and the like can be instances of the more restrictive `MonadTransAskUnlift`.

However, `MonadTransUnlift` also has instances for `StateT` and `WriterT`. These allow correct unlifting without discarding effects (though another function is provided if you want discarding). How is this possible? Magic! `MVar`s! Unlifting `StateT` simply holds the state in an `MVar`. Unlifting `WriterT` uses an `MVar` to collect effects at the end of each unlift.

Using `MVar`s also makes everything thread-safe. Here’s an example:

``````longComputation1 :: IO ()
longComputation2 :: IO ()

ex :: StateT Int IO ()
ex = liftWithUnlift \$ \unlift -> do
a <- async \$ do
longComputation1
unlift \$ modify succ
longComputation2
unlift \$ modify succ
wait a``````

Here, `longComputation1` and `longComputation2` can run in parallel, in different threads. But `unlift` forces synchronisation, meaning that the `modify` statements never overlap. Instead, state is passed from one to the other. So `ex` is guaranteed to add two to its state.

As mentioned earlier, the tunnel monads of transformers in `MonadTransTunnel` are all instances of `MonadInner`. But if the transformer is an instance of `MonadTransUnlift`, its tunnel monad will be an instance of the stricter class `MonadExtract`. And if the transformer is an instance of `MonadTransAskUnlift`, then its tunnel monad will be an instance of `MonadIdentity`, monads equivalent to the identity monad.

The Same, but Monads Relative to IO

Often a monad can be understood as some transformer over `IO`. In such a case, we might want to know the properties of that transfomer.

Composing and Stacking Transformers

The `ComposeT` transformer allows you to compose monad transformers (unlike composing monads, there is no restriction on this). Generally speaking, if `t1` and `t2` both have some property, then `ComposeT t1 t2` will have it too.

The `StackT` transformer allows you to deal with whole stacks of transformers, parameterized by a list of their types:

``````type TransKind = (Type -> Type) -> (Type -> Type)

type StackT :: [TransKind] -> TransKind
newtype StackT tt m a = MkStackT (ApplyStack tt m a)

type ApplyStack :: forall k. [k -> k] -> k -> k
type family ApplyStack f a where
ApplyStack '[] a = a
ApplyStack (t ': tt) a = t (ApplyStack tt a)``````

The concepts of “reader”, “writer”, and “state” monads each imply a kind of data: readers have parameters, writers have products, and states have references. And pretty much any monad has exceptions. So, why not make that data explicit, so we can manipulate it directly?

``````data Param m a = MkParam
, paramWith :: a -> m --> m
}

data Ref m a = MkRef
{ refGet :: m a
, refPut :: a -> m ()
}

stateRef :: Monad m => Ref (StateT s m) s

data Prod m a = MkProd
{ prodTell :: a -> m ()
, prodListen :: forall r. m r -> m (r, a)
}

writerProd :: Monad m => Prod (WriterT w m) w

data Exn m e = MkExn
{ exnThrow :: forall a. e -> m a
, exnCatch :: forall a. m a -> (e -> m a) -> m a
}

allExn :: forall m. MonadException m => Exn m (Exc m)
someExn :: forall e m. MonadCatch e m => Exn m e``````

Parameters and references can be mapped by lenses. Not so much products, though there is one thing we can do with them.

``````mapParam :: Functor m => Lens' a b -> Param m a -> Param m b

mapRef :: Monad m => Lens' a b -> Ref m a -> Ref m b

foldProd :: (Applicative f, Foldable f, Applicative m) => Prod m a -> Prod m (f a)``````

Of course, other monads have their own references:

``````ioRef :: IORef a -> Ref IO a

stRef :: STRef s a -> Ref (ST s) a ``````

Odd Stuff

`ReaderStateT` and `TransformT` are odd things that I make use of elsewhere, but don’t really understand. Both of them convert `Param`s into `Ref`s.

``````newtype WRaised f m = MkWRaised (forall a. f a -> m a)
type ReaderStateT f m = StateT (WRaised f m) m

newtype TransformT m a = MkTransformT (forall r. (a -> m r) -> m r)
transformParamRef :: Monad m => Param m a -> Ref (TransformT m) a``````

Not Included

• `ListT`. This does not transform every monad to a monad, so is not a monad transformer.
• Any notion of a “base” monad. While every transformer stack must logically have some base monad, the concept is non-parametric as transformed monads cannot be base monads.
• Lifted “batteries” functions. Just use `lift`.
• An effect system.

And also…

I have substantially expanded, cleaned up and reorganised `witness`, my package for type witnesses, which Monadology makes use of. I have also published `type-rig`, which provides the `Summable` and `Productable` classes used for monad data.

— Ashley Yakeley

Pinafore 0.3

I had more planned for Pinafore 0.3, but two things happened: I found a bug in the type-checker that absolutely had to be fixed, and took me awhile to figure out. And last week I started full-time work, so I wanted to get a version out now, since I won’t have much time to work on Pinafore for about the next year.

List References

The most important new feature is a new kind of reference type. Pinafore 0.2 had `WholeRef`, `SetRef`, and `FiniteSetRef`. 0.3 adds `ListRef`, which `UI.listTable` uses directly. `ListRef` values can track items more accurately than using a `WholeRef` of a list. For example, you can obtain a `WholeRef` for a given item in the `ListRef`, which will keep track of the position of the item in the `ListRef` as other items are inserted and removed.

In future releases, `ListRef` will be the model for other UI elements. For example, a “grid” UI element is naturally a Cartesian product of a list of rows and a list of columns. Operations such as inserting a new row or column thus become straightforward insertions and deletions to two `ListRef`s.

Subsumption Expressions

A new kind of expression, `expr: type`, subsumes the expression to the type. So for example, `3` has type `Integer`, while `3: Number` has type `Number`. Pretty straightforward.

Module-Qualified Names

You can now write, e.g., `UI.listTable` to refer to the `listTable` symbol in the `UI` module. Note that this isn’t just using the namespace, it also “does” the import. In other words, it’s essentially the same as `let import UI in listTable`.

Why, you might ask? Well, Pinafore doesn’t follow Haskell’s example of putting all the `import` statements at top level, because Pinafore has no “top level”. Since this means one can always bury `import` statements deep inside expressions, it’s simpler to just do the import with the module qualification.

Better Type Simplification

Formerly, the type simplifier eliminated one-sided type-variables. A type variable is one-sided if it only appears in positive position, or else only appears in negative position.

This is now more general: the type simplifier now eliminates all fully-constrained type variables. Here’s an example:

``a & Integer -> a | Number``

gets simplified to

``Integer -> Number``

(because `Integer <: Number`).

The idea is that the constraint `a <: T` is equivalent to the equation `a = a & T`. This is a fundamental principle of Algebraic Subtyping that comes from lattice theory, and making the substitution is how type-checking deals with constraints. However, one can also reverse this substitution, to extract constraints. In this case you’d extract the constraints `a <: Integer` and `a :> Number`. Note that because `Integer <: Number`, `a` is “fully constrained”: Pinafore can specialise it either to `Integer` or to `Number`, or indeed any type “in between” (such as `Rational`), without losing any generality. So that’s exactly what it does.

As it happens, one-sided type-variables are a special case of this. For example, the type `a | Text` yields the constraints `a <: None` and `a :> Text`. And obviously `None <: Text`, so `a` is fully constrained, and the type can be simplified to `Text`.

Other Library Changes

• UI stuff is now in a separate `UI` module (which is actually built in a separate Haskell package).
• The `UI` type has been renamed `Element`, with the expectation that it will usually be referred to as `UI.Element`.
• There are some new UI elements for doing CSS styling.
• There are some new functions and some name changes in the `Std` library. It’s still early for the Pinafore project as a whole, so expect a certain amount of incompatibility between versions.

Next Milestone

My plans for 0.4 are basically everything I dropped from 0.3:

• Graphics, such as how to display images and diagrams in UI elements (earlier awkward Haskell library issues have now been sorted)
• Files, which are the easiest way of handling large blobs of data such as images, video, etc.
• New reference type for text

Release

Version 0.3 of Pinafore is available from Github as a Debian package. There’s also a syntax-highlighting extension for Visual Studio Code.

The Pinafore website has all the documentation.

— Ashley Yakeley

Pinafore 0.2

Pinafore was originally motivated by my desire to organise and structure (i.e., type) various bits of information relating to my life. This is why, for instance, the example Pinafore code in the documentation relates to contacts and events. After I released Pinafore 0.1, I spent some time actually trying to do this, and ran into a number of problems. 0.2 was originally going to be a bigger, longer, milestone, but instead I made fixing these problems a priority. As a result, Pinafore 0.2 is much more pleasant and usable than Pinafore 0.1.

These are the main new features.

Module System

There are now two kinds of Pinafore file, scripts and modules. Scripts are typically UNIX executable files with no filename extension and `#!/usr/bin/pinafore` at the top. A script contains a single expression.

Modules are located in one of a number of known places with filenames that end with `.pinafore`. The contents of a module file generally looks like `let <bindings> in export <names>`.

Recalling that there is no “top level” in Pinafore, both scripts and modules can import modules into any scope with an `import` statement inside a `let` expression.

Anyway, it all works the way you’d expect. Here’s an example.

Dynamic Supertypes

In algebraic subtyping, every subtype relation `P <: Q` implies an “upcasting” conversion function of type `P -> Q`. The overall system of conversion functions needs to be consistent, of course, but apart from that, there’s no restriction on what these functions do. In particular, they do not need to be injective, and retraction functions (“downcasting”, of type `Q -> Maybe P`) do not need to exist.

However, for some subtype relations, a retraction function is available. Pinafore now provides a general mechanism for making use of them.

Every (ambipolar) type `T` has a greatest dynamic supertype `D(T)`, with these properties:

• `T <: D(T)` (“supertype”)
• `D(D(T)) = D(T)` (“greatest”)
• There exists a special form `check @T: D(T) -> Maybe T` (“dynamic”)

There’s now a new kind of pattern that can be used to match according to the retraction function: `(pat: T)` has type `D(T)` and matches `pat` as type `T`.

There are actually two special forms, `check` and `coerce`. They can be defined in terms of the pattern, more-or-less like this:

``````check @T: D(T) -> Maybe T;
check d = case d of
(t:T) -> Just t;
_ -> Nothing;
end;

coerce @T: D(T) -> T;
coerce d = case d of
(t:T) -> t;
_ -> error "coercion from <D(T)> to <T> failed";
end;``````

So what are the greatest dynamic supertypes of various types? In most cases, `D(T) = T`, not very interesting. We do have `D(Integer) = D (Rational) = Number`. But the real motivator is dynamic entity types, see below. For these, `D(T) = DynamicEntity`.

For the future, it actually wouldn’t be hard to introduce predicate types. Given a type `T` and a function of type `T -> Boolean`, one would be able to define a subtype `P` of `T` consisting of those values that satisfied the function. This would be an obvious choice for the dynamic supertype mechanism (with `D(P) = D(T)`, of course). However, for the time being I don’t have a strong motivation for predicate types, so Pinafore 0.2 does not provide them.

Dynamic Entity Types

So generally, Pinafore erases types. There is no information about entity types in storage, nor about which values have which types. This is helpful for reasoning about storage, and for refactoring your schema. However, sometimes you do want store some kind of type information. For example, you might want to implement something like this:

``````Human <: Animal
Dog <: Animal
dateOfBirth: Animal ~> Date
animalUI: Animal -> UI``````

In this case, you do want to store type information for each `Animal`: you want to know whether it’s a `Human` or a `Dog`.

This is how you’d do this with dynamic entity types:

``````dynamictype Human = !"mytype.Human";
dynamictype Dog = !"mytype.Dog";
dynamictype Animal = Human | Dog;
dateOfBirth = property @Animal @Date !"Animal.dateOfBirth";
animalUI animal = case animal of
(human: Human) -> humanUI human;
(dog: Dog) -> dogUI dog;
end;``````

All dynamic entity types are subtypes of `DynamicEntity`, which internally encodes a pair of anchors, one for type and one for “value”. A dynamic entity type simply represents a set of type anchors: in the example, `Human` and `Dog` are each one anchor (as given), and `Animal` is both of them.

A dynamic entity type is concrete if it represents only one type anchor. Given a concrete dynamic entity type, one can generate new values dynamically or statically with the `newDynamicEntity` and `dynamicEntity` special forms.

Comparing the type system of Pinafore to that of, say, Java, there seems to be a certain sense in which dynamic entity types resemble Java’s classes, and open entity types resemble interfaces. I’m not sure how far this intuition goes, though.

Generalised Open Entity Subtypes

Previously, subtype relations could be declared with `subtype P <: Q`, with `P` and `Q` both open entity types. This is now generalised so that `P` can be other (ambipolar) entity types.

But this gives rise to a problem: we cannot have (or at least make use of) more than one subtype relation for a given “ground type constructor” if their parameters are incompatible. Consider this:

``````opentype P;
opentype Q;
subtype Maybe Integer <: P;
subtype Maybe Boolean <: Q;
f: Entity -> ()
f _ = ()
g x = f (Just x)``````

Here the ground type constructor is `Maybe`, so what is the type of `g`? There are two different subtype “paths” to get from `Maybe a` to `Entity`, so we want something like `g: (Integer | Boolean) -> ()`. But that is not allowed, as `Integer | Boolean` is not a negative type.

The solution for the time being is simply to disallow subtype relations on parametered types (such as `Maybe Integer`). This isn’t perfect, but overall an improvement.

Command-Line Arguments & UNIX Environment

If you make a script, you may wish to pass arguments to it when invoking from the command line. If so, `scriptArguments` is what you want. There’s also `scriptName`, `environment`, and `getEnv`.

Next Milestone

My 0.3 plans are still quite fluid, but the main points are:

• Graphics, such as how to display images and diagrams in UI elements (involves some awkward Haskell library issues)
• Files, which are the easiest way of handling large blobs of data such as images, video, etc.
• New reference types for text and for lists.

Release

Version 0.2 of Pinafore is available from Github as a Debian package. There’s also a syntax-highlighting extension for Visual Studio Code.

The Pinafore website has all the documentation.

— Ashley Yakeley

For some reason GADTs are a particular sticking point for many advocates of Simple Haskell. But sometimes GADTs are the natural form of expressing a concept.

By way of example, here’s a snippet of API I’ve borrowed from JuicyPixels:

``````data Image a = Image {
imageWidth :: !Int,
imageHeight :: !Int,
imageData :: Vector (PixelBaseComponent a)
}

data DynamicImage =
ImageY8 (Image Pixel8) |
ImageY16 (Image Pixel16) |
ImageY32 (Image Pixel32) |
ImageYF (Image PixelF) |
ImageYA8 (Image PixelYA8) |
ImageYA16 (Image PixelYA16) |
ImageRGB8 (Image PixelRGB8) |
ImageRGB16 (Image PixelRGB16) |
ImageRGBF (Image PixelRGBF) |
ImageRGBA8 (Image PixelRGBA8) |
ImageRGBA16 (Image PixelRGBA16) |
ImageYCbCr8 (Image PixelYCbCr8) |
ImageCMYK8 (Image PixelCMYK8) |
ImageCMYK16 (Image PixelCMYK16)

promoteImage :: ColorConvertible a b => Image a -> Image b ``````

JuicyPixels was originally released in 2012, and there’s always a good presumption against changing an API, so we can’t blame the developers for not making use of GADTs. But if we were starting a project like this from scratch today, how would we write such code, using the whole language?

The way `DynamicImage` has been defined makes it a bit difficult to work with. For example, if you want to get the width or height of a dynamic image, you’ll have to write cases for each constructor. And the convertibility from one pixel type to another is encoded at the type level (with `ColorConvertible`), but there’s no clean way to do it at the value level, if we wanted to provide that functionality dynamically.

We can make this code more expressive, and more elegant, by using a GADT that represents the pixel type of a dynamic image:

``````data PixelType a where
PixelType8 :: PixelType Pixel8
PixelType16 :: PixelType Pixel16
PixelType32 :: PixelType Pixel32
PixelTypeF :: PixelType PixelF
PixelTypeYA8 :: PixelType PixelYA8
PixelTypeYA16 :: PixelType PixelYA16
PixelTypeRGB8 :: PixelType PixelRGB8
PixelTypeRGB16 :: PixelType PixelRGB16
PixelTypeRGBF :: PixelType PixelRGBF
PixelTypeRGBA8 :: PixelType PixelRGBA8
PixelTypeRGBA16 :: PixelType PixelRGBA16
PixelTypeYCbCr8 :: PixelType PixelYCbCr8
PixelTypeCMYK8 :: PixelType PixelCMYK8
PixelTypeCMYK16 :: PixelType PixelCMYK16

data DynamicImage = forall a. DynamicImage (PixelType a) (Image a)``````

Any code to get properties of the contained `Image` is now much simpler:

``````dynamicImageSize :: DynamicImage -> (Int, Int)
dynamicImageSize (DynamicImage _ img) = (imageWidth img, imageHeight img)``````

We can also express convertibility dynamically, if we want to add that:

``````canPromotePixel :: PixelType a -> PixelType b -> Maybe (Dict (ColorConvertible a b))
-- provided as appropriate

promoteDynamicImage :: DynamicImage -> PixelType b -> Maybe (Image b)
promoteDynamicImage (DynamicImage pta img) ptb = do
Dict <- canPromotePixel pta ptb
return \$ promoteImage img``````

You can see how with Haskell’s fancy shiny GADT feature, the code is now more expressive, and easier to understand for anyone who knows the language.

GADTs are actually not a particularly difficult concept to learn, for someone who already understands rank-n types and existential quantification. And in many situations, they provide a huge benefit in expressibility.

— Ashley Yakeley

The promise of Haskell over other languages is that it allows you to more cleanly and intuitively represent the application domain. This leads to more intelligible and maintainable code. But to take full advantage of what Haskell has to offer, you have to embrace the whole language. This means making use of any appropriate language feature, just as you would with any other language.

If you’re using Haskell in industry, it’s my belief that restricting your team to some “simple” subset of the language for complex problems will make your code more complex and more difficult for competent developers to understand. It will be more likely to have repetitive boilerplate, and more likely to require explicit error calls to handle “impossible” cases. It will be less comprehensible, and so less maintainable.

Here are some claims from “The Simple Haskell Initiative”, which I believe are flawed:

Fancy Haskell is costly to teams because it usually takes more time to understand and limits the pool of people who can effectively contribute.

By taking this attitude, you are not only committing your code to mediocrity, but your team too. Whole, elegant, Haskell, firing on all language cylinders, takes less time for competent developers to understand. And you can raise less-experienced developers to the necessary competence specific to your project.

Things that have been around longer will be more well-tested and understood by a larger group of people. Prefer tried and true techniques over the latest shiny library or language feature. The more foundational something is in your tech stack, the more conservative you should be about adopting new versions or approaches to that thing.

These are two separate things.

For libraries, maturity is certainly a valid concern. But it is unrelated to the structure of the library’s API.

For language features, the GHC team has a high bar for releasing new extensions, often involving formal proof. The implementation of features considered “fancy”, such as GADTs, type families, and polykinds, is understood to be as sound as that of any other part of the language. They are unlikely to be a particular source of compiler defects.

If you adopt a new thing, how much of its complexity will spread throughout the rest of your codebase? You should be more hesitant to adopt something if its complexity is going to spread through a larger portion of your codebase.

Code written in whole Haskell is less complex than “simple” Haskell for the same complex application. That’s the whole point of it.

There is no one definition of what language features count as “Simple Haskell”. Michael Snoyman seeks to define a “boring” subset of Haskell, but his recommended set of “boring” language extensions is quite broad, including most extensions relating to classes and type families, and even `PolyKinds`. Boring Haskell, in practice, seems to be close to Whole Haskell.

Sam Halliday, by contrast, seeks a vastly more restricted language, rejecting GADTs, type families, multi-parameter classes, and apparently even rank-n types and existential quantification. Such restrictions lead to unnecessarily complicated code, in my view. Here’s a simple example of how GADTs and existential data quantification can improve code generality and intelligibility.

What you should be doing

• Embrace the whole language.
• Set a high quality bar for code within your team.
• Mentor less-experienced developers.

Embrace the whole language. Pretty much every “fancy” feature of the whole GHC Haskell language has a productive purpose. That’s the point of all the academic research. As a competent Haskell developer, you should know when that purpose applies and how to make best use of each feature.

Note that language features are not exactly the same as language extensions. For example, the language gives you the option to either allow or prohibit “incoherent” use of class instances. In most cases, the best use of this language feature is to prohibit, as it can ensure a discipline that leads to more intelligibility and predictability.

Some language features are of relatively specialised use. Polykinded types are very useful for type-oriented applications (such as implementing a typed language interpreter). And, of course, some simpler or more straightforward projects might make use of relatively few language features.

Set a high quality bar for code within your team. Set code expectations as early as you can. Discuss ideas early, and make suggestions for design approaches. Haskell makes refactoring easier than many languages, take advantage of that as appropriate.

Mentor less-experienced developers. When you hire a Java, Python, or C++ developer, you can expect them to be fully competent in each of those languages. You can typically give them development ownership of progressively larger project features, and leave them to get on with it until code review. Given the current state of the Haskell job market, this may not be the case for Haskell developers.

If you hire junior developers who are not yet familiar with the whole language, you will need to mentor them. Take extra time with them to explain how features of the Haskell language work, how they are best used in general, and how you use them in your codebase.

If that sounds like an extra burden, bear in mind that not many developers make the effort to learn Haskell in the first place, and those that do are likely to have more aptitude to learn more about it. Invest in the people you hire. If you’re doing anything worthwhile, you’re in this for the long term.

… Why did you choose Haskell, anyway?

— Ashley Yakeley

Pinafore 0.1

We all generate a lot of information in our lives and in our work:

contacts, events, emails, tasks, photos, plans, budgets, financial records, media collections…

Computers are supposed to help us organise it all. So how’s that working out?

For the most part, we use application programs. Each application program works with information of a particular kind, with a polished and specific user interface. However, it fixes a particular schema for that information, and it is typically difficult to combine information from multiple applications.

Alternatively, we can work with information more loosely and flexibly in a spreadsheet. However, this provides a more limited user interface experience, and the very looseness makes it difficult to reason abstractly about the type and schema of the information.

Pinafore is an attempt to reimagine how computers represent and store information, and how users interact with it. It allows users to create their own schemas for information, and create their own interfaces to it.

This 0.1 release includes some of the major pieces: a type system for information, a language, a storage system, some composable user interface elements. Enough to get the gist of the project, and perhaps suggest some future possibilities. But much more needs to be done.

Language

Pinafore is an interpreted language. Information is stored as predicate/subject/object triples in a database in your home directory, and the user interfaces are created with GTK+.

Pinafore generally resembles Haskell. It has a type system derived from Hindley-Milner, and features pattern-matching, lazy evaluation, and separation of pure functions from executable actions. There are some differences however:

• There is no “top level”. A Pinafore file consists of a single expression. Type declarations, like bindings, are declared within `let` expressions.
• Layout is not syntactically significant. Instead, lines are terminated by semicolons, and `do` and `case` expressions are terminated with the `end` keyword.
• The colon is used for type signatures, while the double colon is used for list construction, the other way around from Haskell.
• Line comments start with `#`, while (nestable) block comments are marked with `{#` and `#}`.
• Only one equation is allowed for a function definition. Argument patterns can be matched with `case` expressions.

Of course, there are many features of Haskell that Pinafore lacks, and vice versa.

Type System

Pinafore is a strongly-typed language. The type system implements Stephen Dolan’s Algebraic Subtyping, which is an extension of Hindley-Milner to allow subtyping. This type system is decidable: if an expression has a type, Pinafore can always infer a principal type for it. Like Haskell, however, you can also add type signatures to definitions.

A subtype relation `P <: Q` is a relationship between two types, “P is a subtype of Q”, which simply means “every P is a Q”, or “allow a P where a Q is expected”. Of course, this implies an inclusion function `P → Q` that actually converts the P to the Q. These functions do not have to be injective, nor does there need to be any kind of reverse function `Q → Maybe P`, though these do exist in Pinafore in some cases.

Two types are equivalent if each is a subtype of the other.

Polarity

The type system distinguishes positive and negative types. This is necessary, because certain type operations are only permitted with certain polarities:

• A positive type is a type that can appear in a positive position. Think of this as the type of a value you’ve defined in your program. The type signature of a value is such a positive position.
• A negative type is a type that can appear in a negative position. Think of this as the type of acceptance of values, such as the argument of a function type (that is itself positive).
• An ambipolar type is a type that is both positive and negative. This includes simple types such as `Text`, `Integer`, and so forth.
• If `P` and `Q` are positive types, then `P | Q` is a positive type. You can read this as “a `P` or a `Q`, not telling you which”. As you might expect:
• `P <: P | Q`
• `Q <: P | Q`
• If `P <: R` and `Q <: R`, then `P | Q <: R`.
• If `P` and `Q` are negative types, then `P & Q` is a negative type. Think of this as “must be both a `P` and a `Q`“. Likewise:
• `P & Q <: P`
• `P & Q <: Q`
• If `R <: P` and `R <: Q`, then `R <: P & Q`.
• `None` is a positive type, that is empty (and is a subtype of every type). `None | P` = `P`.
• `Any` is a negative type, that accepts anything (and is a supertype of every type). `Any & P` = `P`.

Here are some examples of expressions with the principal types that Pinafore will infer. Note that Pinafore uses a single rather than double colon for type signatures:

``````\x -> 3: Any -> Integer
Nothing: Maybe None
\b -> if b then "hi" else 3: Boolean -> (Text | Integer)
\x -> x + textlength x: (Integer & Text) -> Integer``````

Type Constructors

Like Haskell, Pinafore has type constructors such as `Maybe`, `[]` (list), `(,)` (pair), `->` (function) and so on. But all type parameters must be types (i.e. as if of Haskell’s kind `*`): in addition, each parameter must be either covariant or contravariant. This gives subtype relations. For example, suppose `F` is a type constructor with one argument:

• If `F` is covariant in its argument, then,
• `F x` has the same polarity as `x`.
• `P <: Q` implies `F P <: F Q`.
• If `F` is contravariant in its argument, then,
• `F x` has the opposite polarity as `x`.
• `P <: Q` implies `F Q <: F P`.

Of course, some types are, morally, neither contravariant nor covariant in their arguments. For these we use a pair of type parameters in a special syntax, one contravariant (marked with `-`) and one covariant (marked with `+`). For example, the `WholeRef` type constructor represents references with get and set operations:

``````WholeRef {-p,+q}
get: WholeRef {-p,+q} -> Action q
(:=): WholeRef {-p,+q} -> p -> Action ()``````

Pinafore has some abbreviations to make working with these a little easier, e.g. `WholeRef T` = `WholeRef {-T,+T}`, and `WholeRef +T` = `WholeRef {-Any,+T}`, etc.

Recursive Types

Pinafore has “equirecursive” types, written in the form `rec v. T`, where `T` is a type expression where `v` appears only covariantly. The key fact of recursive types is that they are equivalent to their unrolling. For example, these two types are equivalent:

``````rec a. (a, Maybe a)
(rec a. (a, Maybe a), Maybe (rec a. (a, Maybe a))``````

Recursive types are necessary for principality (that all typeable expressions have a principal type), though they’re not much used in practice.

Data Types

Pinafore allows you to create your own algebraic data types, like the `data` keyword in Haskell. Here’s an example:

``datatype StopwatchState = StoppedState Duration | RunningState Time;``

Typed Storage

Pinafore stores “knowledge” as relationships between entities of various types. The relationship types are called morphisms, which can be composed as the name suggests.

Types of entities are all subtypes of the `Entity` type. These include:

• Literal types for small pieces of data, such as `Integer`, `Number`, `Boolean` etc.
• Open entity types, that simply represent arbitrary points, declared with the `opentype` keyword. Values of open entity types can be declared statically (with an anchor) with the `openEntity` keyword, or generated at run-time with the `newOpenEntity` function.
• Closed entity types, that have constructors, declared with the `closedtype` keyword. These are similar to data types, except that each constructor has an anchor, and the contained types must themselves be entity types.

Anchors are 256-bit values usually hashed from a literal string in your program. Pinafore erases types when storing information in its storage: it does not store the structure of types nor does it store which values have which types. Instead, it uses anchors to identify information in storage.

Open Entity Example

Here’s an example. Let us suppose to store two relationships concerning people:

• The name of some person p is “James”.
• The mother of p is some person q.

Firstly, we will need a type for people. This can be an open entity type: it has no information of its own besides identity: all information about people comes from morphisms.

``opentype Person;``

We also need properties for “name” and “mother”. We need to give these anchors, since this is what will identify them in storage, not the names of the language bindings we happen to use.

“Name” is a property from `Person` to `Text`, because the name of a person is text. We give it the anchor `!"myschema.name"`.

“Mother” is a property from `Person` to `Person`, because the mother of a person is a person. We give it the anchor `!"myschema.mother"`.

Properties are morphisms, so the type of them is a morphism type, indicated by `~>`. In fact, properties generate morphisms: you can compose morphisms together that are strings of properties. In this case, you can compose these two to get a morphism for “name of mother”.

``````name: Person ~> Text;
name = property @Person @Text !"myschema.name";
mother: Person ~> Person;
mother = property @Person @Person !"myschema.mother";``````

Now we need entities p and q. These might be generated at run-time or obtained elsewhere, but here we’ll declare them statically. Again, it is the anchor that identifies them in storage, not the bindings `p` and `q`.

``````p: Person;
p = openEntity @Person !"someperson";
q: Person;
q = openEntity @Person !"otherperson";``````

Actually storing the relationships is an `Action` (similar to `IO` in Haskell). And like Haskell, Pinafore has `do` notation to make working with actions easier:

``````do
name !\$ {p} := "James";
mother !\$ {p} := q;
end``````

The `!\$` operator applies a morphism to reference to get another reference. Since `p` is an entity, not a reference, we must first convert it to a reference using “reference notation” `{p}`.

The `:=` notation sets the value of a reference.

Here’s a typed breakdown of that first action:

``````p: Person
{p}: WholeRef +Person
name !\$ {p}: WholeRef Text
name !\$ {p} := "James": Action ()``````

Here’s what it looks like put altogether:

``````let
opentype Person;
name: Person ~> Text;
name = property @Person @Text !"myschema.name";
mother: Person ~> Person;
mother = property @Person @Person !"myschema.mother";
p: Person;
p = openEntity @Person !"someperson";
q: Person;
q = openEntity @Person !"otherperson";
in do
name !\$ {p} := "James";
mother !\$ {p} := q;
end``````

This is a complete Pinafore program. Running it will store those two relations in Pinafore’s persistent storage.

Of course, we can combine the morphisms in other ways:

``````# everyone who's mother's name is Kate
(name !. mother) !@ {"Kate"}

# the (name, mother) pair of p
(name !** mother) !\$ {p}``````

It is important to note that Pinafore does not store entities per se, it stores relations between entities. One cannot, for example, retrieve all entities of type `Person`. Types of entities such as `Person` are erased for storage. However, one can retrieve all entities that have name “James”, or whose mother is some entity `q`.

Closed Entity Types

Closed entity types resemble data types, but they are all subtypes of `Entity`, and so can be stored. Every constructor of a closed entity type includes an anchor, to identify that constructor in storage. Here’s an example:

``````closedtype CelestialLocation
= EquatorialLoc Number Number !"EquatorialLoc"
| EclipticLoc Number Number !"EclipticLoc";``````

Reinterpretability

Any item of information retrieved from storage can be “unknown”, and Pinafore is robust with regards to what it happens to find in storage. This gives a certain amount of flexibility in modifying an existing “schema”, or system of entity types, without having to transform data in storage. For example, if you remove a property from your program, Pinafore will simply ignore that information in storage. If you add a property, Pinafore will initially find all values of that property to be “unknown”. Constructors can be added and removed from closed entity types. If Pinafore finds something it doesn’t recognise or cannot parse as it expects, it treats it as “unknown”.

Composable User Interface Models

In terms of the Model/View/Controller way of looking at user interface, the view and controller are represented by user interface elements (of type `UI`), while the model is represented by references (of type `WholeRef`, `SetRef`, and `FiniteSetRef`).

A reference represents the state of some thing. The user may wish to retrieve some part of that state, or make some change to it, or be notified when it changes. References are thus “live”: when connected to a UI element, the user can use the UI to change the reference, but also the reference can update the UI when its state changes.

• Whole references (`WholeRef`) represent a single value (which might be “unknown”). There are operations for getting, setting, and deleting (making unknown).
• Set references (`SetRef`) represent some arbitrary set or predicate of some type. There are operations for adding and removing members, and for checking membership of some value.
• Finite set references (`FiniteSetRef`) are set references that have a finite number of members, that can be retrieved.

The various kinds of references can be composed in various ways, such as various set operations (union, intersection, Cartesian product and sum).

Pinafore’s “reference notation” makes working with whole references a little easier. For example, given two whole references to integers, we can create a new whole reference that is the sum of them:

``````p: WholeRef Integer;
q: WholeRef Integer;
pq: WholeRef +Integer;
pq = {%p + %q};``````

Whenever `p` or `q` updates, then `pq` also updates. Of course, `pq` is read-only: attempts to set it will fail.

User Interface Elements

User interface elements are things such as text areas, buttons, check boxes, and tables. They are constructed from the references they control, and can be composed by horizontal or vertical layout, and put in windows.

Release

Version 0.1 of Pinafore is available from Github as a Debian package.

The Pinafore website has all the documentation.

— Ashley Yakeley