Write You a Programming language for Computable Functions: Syntax

This post is the first one in a series where I will walk through the implementation of an untyped version of PCF¹ in Haskell.

I will extend the original PCF with constant naturals, the basic arithmetic operations \(+, -, \times, /\), a list datatype with the primitive functions cons, head, tail and null. In addition, I add let ... in ... and let rec ... in ... constructs as syntactic sugar.

The complete source code is available on github. The structure of the project closely follows Write You a Scheme. The inside is inspired by Stephen Diehl’s Write You a Haskell.

In this post I will describe the AST of my implementation.

Here is a description of the original PCF without its types in the BNF formalism:

$$ \begin{align} \langle Expr \rangle ::=&\ 0\ |\ true\ |\ false \\
&|\ \langle var \rangle \\
&|\ succ( \langle Expr \rangle ) \
|\ pred( \langle Expr \rangle ) \
|\ iszero( \langle Expr \rangle ) \\
&|\ if\ \langle Expr \rangle\
then\ \langle Expr \rangle\
else\ \langle Expr \rangle \\
&|\ \langle Expr \rangle\ \langle Expr \rangle \\
&|\ \lambda \langle var \rangle . \langle Expr \rangle \\
&|\ \mu \langle var \rangle . \langle Expr \rangle \end{align} $$

In PCF, the numbers are the non-negative integers and are built from the constructor \(0\) and the combinators \(pred\) and \(succ\). Conditional expressions are represented here by the \(if … then … else …\) construct. The expression after \(if\) must evaluate to one of the constructors \(true\) or \(false\). In case of \(true\), the entire conditional expression has the same result as the expression that follows \(then\), otherwise its result is that of the expression that follows \(else\). Function abstraction and application have the same shape as in the lambda calculus. And recursion is expressed with the \(\mu\) operator. Using the fixpoint operator, this expression for recursion can be written as \( Fix(\lambda \langle var \rangle . \langle Expr \rangle)\).

In my implementation, numbers are the inhabitants of Haskell’s Integer type. The boolean constructors \(true\) and \(false\) are from Haskell’s Bool type. Lists of PCF expressions are formed with the help of Haskell’s List. Without forgetting the binary operators, these considerations lead us to the following Haskell representation

data Expr
  = Var String
  | Nat Integer
  | Bool Bool
  | List [Expr]
  | App Expr Expr
  | Lam String Expr
  | Mu String Expr
  | If Expr Expr Expr
  | PrimOp PrimOp Expr
  | Op BinOp Expr Expr
  | Undefined
  deriving (Show, Eq)

data PrimOp
  = Succ
  | Pred
  | IsZero
  deriving (Show, Eq)

data BinOp
  = Add
  | Sub
  | Mult
  | Div
  deriving (Show, Eq)

That is all we need to represent the version of PCF I want to present. In the next post I will describe the parsing of text into this AST.

Bibliography