Bernard Sufrin, November 29, 2025
PicoML is a polymorphically-typed lazy functional language with I/O actions (cf the I/O Monad in Haskell). It has a very flexible concrete syntax, and a very straightforward polymorphic type system. Its only implementation - a prototype - is written in OCaml as direct, closure-based, abstract-syntax tree interpreter. PicoML GitHub Repository
We would like to see a more efficient implementation, as well as one that would make it straightforward to incorporate new features for engaging with external entities (graphics, etc)
The present project would reimplement the language in one or both of the following ways, each of which would first require a reimplementation of parser and type checker -- possibly, but not necessarily, in Scala.
as a closure-based, abstract-syntax tree interpreter using continuations.
as a (Scala) compiler translating to code for an abstract machine - possibly the G-Machine of Lennart Augustsson and Thomas Johnsson - thence to executable code for conventional architecture.
The outcome of the project should be both useable and scrutable: students should be able to read the code of a realistic language implementation.
We think that the PicoML language implementation described above would be a very good basis for a new implementation of a simplified variant of Haskell, suitable for introducing that language in such a way that the need for type classes emerges organically from programming practice.
The project would aim to deliver an implementation suitable for use by Haskell novices that would place emphasis on good error diagnostics: both type errors and runtime errors. Availability of such an implementation could make the teaching of functional programming is the secondary school CS curriculum and for home study a practical proposition: thereby liberating at least some pupils from the conceptual straightjackets of Python, C++, etc.
An important difficulty students have with Haskell and its type system is the (important) notion of type classes: whilst very useful to more advanced Haskell users, they can pose a barrier to learning because what might (in their absence) be a type-error that is straightforward to report and to diagnose, gets reported in terms of instances and classes. For example:
ghci> max xs
<interactive>:2:1: error:
• No instance for (Show ([Integer] -> [Integer]))
arising from a use of ‘print’
(maybe you haven't applied a function to enough arguments?)
• In a stmt of an interactive GHCi command: print it
ghci> max
<interactive>:1:1: error:
• No instance for (Show (() -> () -> ()))
arising from a use of ‘print’
(maybe you haven't applied a function to enough arguments?)
• In a stmt of an interactive GHCi command: print itOf course wise neophytes take their tutors' advice, and explore the type of the function they thought they were using correctly:
ghci> :t max
max :: Ord a => a -> a -> aand may then realize that what they were after is
ghci> :t maximum
maximum :: (Foldable t, Ord a) => t a -> aBut what's a Foldable? The neophyte has to understand
that it's a constructor class! And the most succinct
explanation of that that can be found is
"A constructor class is declared with a type parameter of kind
* -> *, * -> * -> *In other words: a constructor class describes behaviour of type constructors, not of ground types."
Thus in order to understand an inscrutable diagnosis of simple mistake made in writing in a simple language, our neophyte must take on board explanations of advanced ideas (type class, kind, etc) that can only be understood once the simpler language has been mastered.
The purpose of this project would be to implement an interactive system to support the discovery (and pretty presentation) of equational proofs by a combination of "automatic choice" and human guidance. Richard Bird, acknowledging Mike Spivey's unpublished work, sketched an implementation of the simplest form of such a "proof assistant" in Haskell in his most excellent book: Thinking Functionally with Haskell. The project would start by implementing a similar assistant with a convenient interactive workflow for discovering, recording, and checking proofs.
The tool should also support the use of appropriate induction rules derived automatically from data declarations.
An interesting challenge will be the provision of convenient methods for providing human guidance for the application of algebraic laws (such as associativity, commutativity, distributivity) at appropriate points in a proof. Although now somewhat long in the tooth, the Jape generic proof editor still provides (in its functional programming example theory) a working concrete example of the sort of guidance that could be used here, and a user interface by which such guidance can be communicated. Our slogan while building Jape (and many of its example theories) was "Proof by Pointing". The Jape GitHub repository is here.
Many Haskell proofs take the form of straightforward equational rewriting using definitions or derived laws left-to-right as rules. Typically the discovery of a proof of
lhs = rhswill take the form
lhs
= { rule name
lhs1
= { rule name
lhs2
.
lhsn
= { rule name}
crux followed by
rhs
= { rule name
rhs1
= { rule name
rhs2
...
rhsm
= { rule name
cruxWhere crux is the common term to which both sides can be
reduced. This style of presentation relies implicitly on the
transitivity of equality.
Aside: it is annoying that some authors obfuscate these sensible discovery steps by a linearised presentation "as if" the post-crux proof had been discovered by using rules ``right to left''
...
crux
= { rule name
rhsm
= { rule name
...
rhs2
= { rule name
rhs1
= { rule name
rhsIn our experience such presentations can be pedagogically harmful.
Sometimes the choice of rule at each stage is almost automatic: "pretend you are the Haskell interpreter". At other times firm human guidance (and/or the invention of lemmas) is needed. For example, a proof of
(rev * rev) . swap . (rev * rev) . swap
=
...
=
idin the presence of laws/definitions
rev . rev = id
swap(y,z) = (z,y)
(f * g)(y, z) = (f x, g y)can use the lemmas
swap . (f*g) . swap = g*f
(f * g) . (h *j) = (f . h) * (g . j)as well as timely invocation of the associativity of composition.