HML is a toy functional programming language inspired by ML (as well as Haskell). Its properties and features include:
- a Hindley-Milner-like type system including
- Hindley-Milner type inference (type annotations are never necessary)
- existential quantification
- optional type annotations almost anywhere
- prenex polymorphism of functions and datatypes
- algebraic data types
- simple pattern matching
- strict evaluation
- impure functions including I/O and array operations
- compilation to x64 assembly (GAS) with
- direct compatibility with System V AMD64 ABI
- tail call optimization
Some notable features that HML lacks are:
- closures (/ nested function definitions)
- but existential quantification gives DIY closures
- currying (since closures aren't built-in)
- garbage collection
- it makes plenty of garbage! it just doesn't clean up
Let's get to the "Hello, World":
main() = out_string("Hello, World!");
Saving this file to hello.hm
, we can compile and run our program
with the following commands:
cat hello.hm | HMCompile > hello.S # generate x64 assembly
gcc hello.S -o hello # assemble and link
./hello # run!
Additional code examples are available in the sample-src
directory.
The syntax of type expressions looks like this:
t, u, v, w ... -- types
a -- type variables
F -- type constructors
types t ::=
Int -- 64-bit integer primitive type
| String -- opaque String primitive type
| a -- type variable
| F(u, v, ...) -- application of type constructor
| (u, v, ...) -> w -- function type
(ellipsis indicate any natural number of arguments)
There are two sorts of top-level declarations that can be made in HML: data type definitions and function definitions.
Here's data type definition where we define booleans:
data Bool() of True() | False();
Booleans are actually built-in, so this declaration can be found in the
Prelude (Prelude.hm
), whose declarations are automatically inserted before
reading any source file.
We call Bool
a type constructor and True
and False
data constructors.
Effectively, Bool
is a nullary function on types, and True
and False
are nullary functions on terms. Names for type constructors and data
constructors must begin with uppercase variables.
There are two primitive types: Int
, which represents 64-bit signed integers,
and String
, which represents (opaque) strings of ASCII characters. We can
recursively define a linked list of integers like this:
data IntList() of Nil() | Cons(Int, IntList());
Type variables allow polymorphism. Consider a definition of lists polymorphic in the type of their elements:
data List(a) of Nil() | Cons(a, List(a));
Type variables must begin with lowercase letters. Their scope is local to the top-level declaration in which they are used. For data declarations, simply using a type variable as an argument to a type or data constructor introduces it into scope.
Using a type variable in a data constructor, but not in the corresponding type constructor, results in existential quantification. For instance, let's say that we wish to make a datatype representing arguments of two variables for which the first argument has already been applied:
data F(a2, b) of F(a1, (a1, a2) -> b);
(Note that we can use the same name for a type constructor and data constructor , since terms and types are completely different syntactic categories.) It might help to imagine this data declaration as creating a function declaration that looks like this:
F(x : a1, f : (a1, a2) -> b) : F(a2, b) = #magic#;
Here, we see that the function F is universally quantified over the type
variable 'a1'. That means that whenever we inspect a term with type
F(a2, b)
, we don't know the type 'a1', and so we must work with it in a
polymorphic manner.
The term expression language looks like this:
e1, e2, e3 -- expressions
v1, v2, v3 -- variables
t -- type variables
p1, p2, p3 -- productions
F, G, H -- data constructors
expressions e ::=
13 -- integer literal
| "Hello\nWorld" -- string literal
| v1(e1, e2, ...) -- function application
| let v1 = e1 in e2 -- let statement
| case e1 { p1 | p2 | ... } -- case expression
| e : t -- explicit type annotation
productions p ::=
F(v1, v2, ...) => e
Only simple pattern matching is allowed. That is, catch-all patterns like this:
case True() { v => v };
are not allowed, and neither are nested patterns like this:
case And(And(1,2), 3) { And(And(x, y), z) => x + y + z };
Since HML is strict and impure, evaluation order matters. In the case of
function application, arguments are evaluated from left to right. In the
let assignment let v = e1 in e2
, e1
is evaluated before e2
.
The sequencing operator >>
, is simply syntactic sugar:
e1 >> e2 ==> seq(e1, e2)
seq(x, y) = y
Explicit type annotations are never necessary, but they can be of assistance both in developing as well as documenting code. Type variables may be introduced into the scope of a function declaration simply by using them inside type annotations for the arguments or the return type. For example, we can write
seq(x : a, y : b) : b = y;
These type variables are then in scope in the body of the function definition. Type variables cannot be introduced into the scope in any other way. For example, the following is invalid, because the type variable 'a' is not in scope:
myFunction() = Nil() : List(a);
even though this is perfectly acceptable:
myFunction() : List(a) = Nil() : List(a);
Explicit type annotations can allow you to make a function's type more
restrictive than type inference dictates. For example, we can specialize
the seq
function to operate only on integers:
seqInt(x : Int, y : Int) = seq(x, y);