Pinafore 0.2

Leave a reply

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

Leave a Reply