A more elegant weapon, for a more civilised age

Amulet is a simple, modern programming language based on the long tradition of the ML family, bringing improvements from the cutting-edge of programming language research.

Amulet's type system supports many advanced features, including but not limited to:

Simple syntax

let map f = function (* 1 *)
| [] -> []
| Cons (x, xs) -> Cons (f x, map f xs) (* 2 *)

let filter p xs = [ x | with x <- xs, p x ] (* 3 *)
  1. Minimalist syntax: semicolons, in and other noise is entirely optional.
  2. Pattern matching and guards make writing code more intuitive.
  3. List comprehensions are a short and sweet way of expressing complex computations on lists.

Powerful types

type vect 'n 'a =    (* 1 *)
  | Nil  : vect Z 'a (* 2 *)
  | Cons : forall 'a. 'a * vect 'n 'a -> vect (S 'n) 'a

(* 3 *)
let rec map (f : 'a -> 'b) (xs : vect 'n 'a) : vect 'n 'b =
  match xs with
  | Nil -> Nil
  | Cons (x, xs) -> Cons (f x, map f xs)
  1. Types can be parametrised by not only other types, but all manners of data types: type constructors, naturals, integers…
  2. Indexed types let constructors vary their return types, enforcing invariants statically.
  3. Polymorphic type annotations enforce strict contracts on implementations, more often than not forbidding incorrect implementations entirely.

Type-level computation

type function 'n :+ 'k begin  (* 1 *)
  Z      :+ 'n = 'n           (* 2 *)
  (S 'n) :+ 'k = S ('n :+ 'k) (* 3 *)
end

let rec append (xs : vect 'n 'a) (ys : vect 'k 'a) : vect ('n :+ 'k) 'b =
  match xs with
  | Nil -> ys
  | Cons (x, xs) -> Cons (x, append xs ys)
  1. Type functions let the programmer express complex invariants in a functional language rather than trying to wrangle type-level prolog.
  2. Functions at the type level are defined by pattern matching and compute by β-reduction, much like at the value level.
  3. A powerful termination checker ensures that your type-level functions won't send the type checker into a tailspin. Even then, the type checker has resource limits to ensure it does not run away.