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.

Haskellish Things

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
• Threads
• “do” notation, for monads

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

Haskell	Pinafore
v :: T	v: T
\x y -> x + y	fn x, y => x + y
\case	match
x & f = f x	x >- f = f x
case x of	x >- match
h : t	h :: t
()	Unit
Bool	Boolean
[]	List
NonEmpty	List1
(P, Q)	P *: Q
Either P Q	P +: Q
IO	Action

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 <- read.Source someinput;
    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.

14. Composable Asynchronous Tasks

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)

await.Task: Task a -> Action a

check.Task: Task a -> Action (Maybe 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.

Learn More

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

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"
    - add Nix flake
  * 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 min/max/lesser/greater functions
      . 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 Task module
      . add Task type & associated functions
    - new Stream module
      . add sinks & sources
    - new Env module
      . move invocation-type stuff here
      . add stdin, stdout, stderr
    - 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
      . add Image, HasMetadata, PNGImage, JPEGImage types, etc.
    - 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

class MonadThrow e m => MonadCatch e m where
    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.

Composing Monads

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.

Inner Monad

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))

instance (MonadInner inner, Monad outer) => Monad (ComposeInner inner outer)
instance MonadInner inner => MonadTrans (ComposeInner inner)

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.

Outer Monad

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)

class Monad m => MonadOuter m where
    getExtract :: m (WExtract m)

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

instance (MonadOuter outer, Monad inner) => Monad (ComposeOuter outer inner)
instance MonadOuter outer => MonadTrans (ComposeOuter outer)

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

lifecycleOnClose :: MonadAskUnliftIO m => m () -> LifecycleT m ()

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)
(MonadPlus m, Monoid w) => MonadPlus (WriterT w m)
MonadIO m => MonadIO (ExceptT m)

Monadology has a class for this:

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

instance TransConstraint Monad (ReaderT r)
instance Monoid w => TransConstraint MonadPlus (WriterT w)
instance TransConstraint MonadIO ExceptT

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

class (MonadTrans t, TransConstraint Monad t) => MonadTransHoist t where
    hoist :: forall m1 m2. (Monad m1, Monad m2) =>
        (m1 --> m2) -> t m1 --> t m2

class (MonadTransHoist t, MonadInner (Tunnel t)) => MonadTransTunnel t where
    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)

commuteT :: (MonadTransTunnel ta, MonadTransTunnel tb, Monad m) =>
    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)
    getDiscardingUnlift :: forall m. Monad m =>
        t m (WUnlift MonadTunnelIOInner t)

-- | A transformer that has no effects (such as state change or output)
class MonadTransUnlift t => MonadTransAskUnlift t where
    askUnlift :: forall m. Monad m => t m (WUnlift Monad t)

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! MVars! Unlifting StateT simply holds the state in an MVar. Unlifting WriterT uses an MVar to collect effects at the end of each unlift.

Using MVars 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.

Monadology provides classes for such monads, that mirror classes for transformers:

MonadTrans	MonadIO
MonadTransHoist	MonadHoistIO
MonadTransTunnel	MonadTunnelIO
MonadTransUnlift	MonadUnliftIO
MonadTransAskUnlift	MonadAskUnliftIO

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)

Monad Data

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
    { paramAsk :: m a
    , paramWith :: a -> m --> m
    }

readerParam :: Monad m => Param (ReaderT r m) r

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 Params into Refs.

newtype WRaised f m = MkWRaised (forall a. f a -> m a)
type ReaderStateT f m = StateT (WRaised f m) m
readerStateParamRef :: Monad m => Param f a -> Ref (ReaderStateT f m) a

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