Polymorphism

Constraint solving

Polymorphism means literally "to have many forms". There are many different approaches to polymorphism. Object oriented languages usually take a heirarchical approach; every type inherits from another in a tree structure, with the most generic type Object at the very top. Halcyon instead takes a constraint solving approach. Consider this code:

let fizz_buzz = fn num =>
  match (num mod 3, num mod 5) with
    | (0, 0) => "FizzBuzz"
    | (0, _) => "Fizz"
    | (_, 0) => "Buzz"
    -- Otherwise, return the number as a string
    | (_, _) => show num

This let statement introduces two variables with unknown types, fizz_buzz and num. It is possible to deduce what the types should be by looking at context clues. The compiler produces a set of constraints from these clues, for example:

• num mod 3 implies that the mod operator needs to work on 3 (an integer) and whatever type num is.
• fizz_buzz must be a function, and the parameter type must be whatever type num is.
• The return type of fizz_buzz must be whatever value the match expression produces.
• Etc...

After the compiler finds every constraint it can, it tries to "unify", or find a single type which fits every constraint. In this case, there are more than enough information to deduce that fizz_buzz must have the type Integer -> String.

Sometimes unification can fail. This happens when two constraints contradict each other. Consider the expression false + 1 / "foo". The + and / operators both have the constraint that the left and right hand side must be the same type. This means the compiler produces the constraints Boolean = Integer and Integer = String, which cannot be true. When unification fails, Halcyon will produce a type error.

What happens when there are very few constraints? Consider the function identity:

let identity = fn i => i

• i has no constraints at all.
• identity only has the constraint that its parameter and return type are the same as whatever i is.

The identity function is polymorphic, it's type is for a in a -> a. In plain english, this means "Let a be any type at all; identity has the type a -> a". That means we can use identity as if it had the type Integer -> Integer, String -> String, etc. Thinking back on the original definition of polymorphism, identity really does have "many forms".

let identity: for a in a -> a =
  fn i => i
do identity true
do identity 1
do identity "foo"
do identity 'a'

A non-polymorphic type is called "concrete", or "fully-constrained".

Polymorphic Types

Types can be polymorphic as well. The most widely used and useful polymorphic type is Option, which is defined as:

type Option: t =
  | None
  | Some t

let some_int: Option Integer = Some 1
let nothing = None

-- Get the value inside an option,
-- or crash the program if nothing is there
let unwrap: for a in Option a -> a = fn
  | None => panic "Failed to unwrap"
  | Some v => v

The Option type is useful for operations that may fail, like searching a list or reading from a file. Polymorphism allows us to define one reusable Option type instead of many different types. The Result type is like Option, except it can carry error information:

type Result: err ok =
  | Err err
  | Ok ok

let unwrap: for err ok in Result err ok -> ok = fn
  | Err _ => panic "Failed to unwrap"
  | Ok v => v

In the two examples, t, err, and ok are all types parameters. A type parameter is just like a function parameter. You can think of Option and Result like functions that return types. The implications of this go deep, and we will discuss it much more later.