Tutorial 3: Advanced language features

Higher-order polymorphism

The type-and-effect system of Helium is fully kinded and allows for arrow kinds. As a consequence, type parameters can be functions over types. This feature is useful, for example, when we want to separate recursion and the structure of a type.

data rec Fix F = Fix of F (Fix F)

data ListF X L = Nil | Cons of X, L

let unFix (Fix l) = l
let nil       = Fix Nil
let cons x xs = Fix (Cons x xs)

let rec append xs ys =
  match unFix xs with
  | Nil       => ys
  | Cons x xs => cons x (append xs ys)
  end

Polymorphic constructors, fields, and operations

Constructors of ADTs, fields of record, and operations of algebraic effects can be polymorphic and bind their own types.

In the case of ADTs, these types behave like existential types. Here is an implementation of streams that use existential types to hide the implementation of stream state.

data rec Stream X =
| Stream of type S. S, (S -> Pair X S)

let head (Stream s next) = fst (next s)
let tail (Stream s next) = Stream (snd (next s)) next

let nat = Stream 0 (fn n => (n, n + 1))

Alternatively, all lowercase type variables that appears in the definition of type are quatified near the constructor, field or operation. The folowing definition of Stream means exactly the same:

data rec Stream X = Stream of s, (s -> Pair X s)

Analogously, we can define polymorphic fields of record using similar syntax. While defining value of such a record type, polymorphic fields must be given as a value due to value restriction.

data Monad M =
  { unit : type A. A -> M A
  ; bind : (a -> M b) -> M a -> M b
  }

data Id X = Id of X
let idM = { unit = Id; bind = fn f (Id x) => f x }

Finally, operations of algebraic effects can also be polymorphic. This feature allows us to say that operations never returns, as in Error effect.

effect Error = { error : Unit => a }

But we can imagine more interesting use cases, as the following Trace effect, which allows to log a message each time when some expression is evaluated.

effect Trace = { trace : type A. String, A => A }

let hTrace =
  handle
  | trace msg v => printStr msg; resume v
  end

Notice, that type A is universally quatified in the type of operation trace, but in the handler it behaves like an abstract type.

Locally abstract types

Sometimes we provide type annotations to help type-checker to infer types, or just to provide better documentation of the code. But some of type variables are implicitly bound, e.g. existential types, or abstract types in polymorphic functions or in a handler of polymorphic operation. We can give names to that variables by writting pattern like (type A B) in a place where these variables are bound.

data rec Stream X =
| Stream of type S. S, (S -> Pair X S)

let rec map (type X Y) (f : X -> Y) (s : Stream X) =
  let (Stream (type S) t g) = s in
  Stream (t : S) (fn r =>
    let ((a : X), b) = g r in
    (f a), b)

Polymorphic recursion

Locally abstract types are very useful to define polymorphic recursive functions. Here is an example of representing lambda-terms using nested data types approach. Notice that in the Lam case of map and bind functions the recursive calls change the instatiation of types A and B. Without locally abstract types, recursive functions are locally monomorphic. Functions map and bind would not typecheck without type annotations. But we need to provide only a tiny bit of information about types: the type of the expression e in the bind function was inferred.

data Inc V = Z | S of V

data rec Expr V =
| Var of V
| Lam of Expr (Inc V)
| App of Expr V, Expr V

let inc_map f m =
  match m with
  | Z   => Z
  | S x => S (f x)
  end

let rec map (type A B) f (e : Expr A) : Expr B =
  match e with
  | Var x     => Var (f x)
  | Lam e     => Lam (map (inc_map f) e)
  | App e1 e2 => App (map f e1) (map f e2)
  end

let lift f m =
  match m with
  | Z   => Var Z
  | S x => map S (f x)
  end

let rec bind (type A B) (f : A ->[|_] Expr B) e =
  match e with
  | Var x     => f x
  | Lam e     => Lam (bind (lift f) e)
  | App e1 e2 => App (bind f e1) (bind f e2)
  end

let subst e e' =
  bind (fn x =>
    match x with
    | Z   => e'
    | S x => Var x
    end) e

Top-level handlers

You can install handlers in a REPL session using the let handle construct as in the following example.

[IO]> effect IntState =
        { get : Unit => Int
        ; put : Int  => Unit
        } ;;
[IO]> let stateH c =
        handle c () with
        | get () => fn s => resume s  s
        | put s  => fn _ => resume () s
        end 0 ;;
[IO]> let handle stateH ;;
[IntState,IO]> get () ;;
0
: Int
[IntState,IO]> List.iter (fn x => put (get () + x)) [1,2,3,4] ;;
()
: Datatypes.Unit
[IntState,IO]> get () ;;
10
: Int
[IntState,IO]>

This feature is a part of a language and works outside the REPL, but its semantics is very counter intuitive. We believe that usual programmer should not use this construct outside the REPL.

Wiki

helium / popl20 / Tutorial_AdvancedFeatures