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.
The most important new feature is a new kind of reference type. Pinafore 0.2 had
FiniteSetRef. 0.3 adds
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
A new kind of expression,
expr: type, subsumes the expression to the type. So for example,
3 has type
3: Number has type
Number. Pretty straightforward.
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
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
Other Library Changes
- UI stuff is now in a separate
UImodule (which is actually built in a separate Haskell package).
UItype has been renamed
Element, with the expectation that it will usually be referred to as
- There are some new UI elements for doing CSS styling.
- There are some new functions and some name changes in the
Stdlibrary. It’s still early for the Pinafore project as a whole, so expect a certain amount of incompatibility between versions.
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
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