Code for this post is available at 651548ffa8.

To confirm that a function type-checks correctly requires inferring the type of the return value and then checking it matches with the type signature. A return value can either be a function parameter, a return value of an inner expression, or a literal.

(sig return_value_as_parameter [Integer] Integer)
(def return_value_as_parameter [x]
  x)

(sig return_value_from_inner_expression [] Integer)
(def return_value_from_inner_expression []
  (* 3 (+ 1 1)))

(sig return_value_as_literal [] Integer)
(def return_value_as_literal [] Integer
  0)

In each of these cases, we can easily infer the type of the return value is Integer and that it matches with the signature. Things get a bit more complicated when you introduce algebraic data types.

(deftype IntOrString []
  (union [Integer String]))

(sig foo [] IntOrString)
(def foo []
  1)

Now it’s not as simple to compare the inferred type of Integer with the signature’s type of IntOrString. Instead of an exact Integer to Integer comparision, we need to expand1 IntOrString into a list of its possible types, and then compare Integer to each of those until we find a match. If the return type is composed of several other union types, we need to expand recursively to get all possible types.

Recursive expansion does expose the possiblity of an infitie recursive type, like those that define lists and trees. The current version of the Erie compiler will infitie loop when it finds a type like this; fixing that will come later.

(deftype RecursiveList [a]
  (union [{a nil} {a (RecursiveList a)}]))

; instance of (RecursiveList Integer) might look like
; {4 {3 {2 {1 nil}}}}

(deftype RecursiveTree [a]
  (union [{'leaf a} {'left (RecursiveTree a) 'right (RecursiveTree a)}]))

; instance of (RecursiveTree Integer) might look like
; {'left {'leaf 1} 'right {'left {'leaf 2} 'right {'leaf 3}}}

As of today, the Erie compiler is about as naive as it gets when it comes to type expansion. It all happens just-in-time and nothing is cached. This means every time the compiler encounters a signature with a return value of IntOrString, it will completely expand it and check, then throw everything away. This is no doubt the slowest way to do type checking, but it was the simplest way for now.

  1. I'm using the phrase "type expansion", but I don't know if that is the phrase favored by compiler authors. My googling efforts have been fruitless. It makes sense to me so I'm sticking with it.