A simple, functional programming language in the ML tradition

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:

- Generalised Algebraic Data Types (GADTs),
- Multi-parameter type classes with
*associated types*and*functional dependencies*, including support for quantified constraints, - Type functions supporting dependent kinds, and equality constraints,
- Rank-N, impredicative types via Quick Look: ∀ quantifiers can appear anywhere in a type, not only the top-level,
- Principled, extensible records via row polymorphism support inference of principal types.

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 *)

- Minimalist syntax: semicolons,
`in`

and other noise is entirely optional. - Pattern matching and guards make writing code more intuitive.
- List comprehensions are a short and sweet way of expressing complex computations on lists.

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)

- Types can be parametrised by not only other types, but all manners of data types: type constructors, naturals, integers…
- Indexed types let constructors vary their return types, enforcing invariants statically.
- Polymorphic type annotations enforce strict contracts on implementations, more often than not forbidding incorrect implementations entirely.

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)

- Type functions let the programmer express complex invariants in a functional language rather than trying to wrangle type-level prolog.
- Functions at the type level are defined by pattern matching and compute by β-reduction, much like at the value level.
- 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.