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.

Updates

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 ListRefs.

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

Updates

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

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

Some of the design has changed since then. I’ve also fixed the UI performance.