Functions

fun x -> x

forall a. a -> a

The identity function has no constraints on x, so its type is quantified over all a. Read forall a. a -> a as "for any type a you pick, this is a function that takes an a and returns an a" — so id can be called on a number and return a number, on a string and return a string, etc. The a is chosen fresh at every use site. The -> arrow reads "takes … returns".

X.Fun (X.Ident "x") (X.Var "x")
|> solve [] None
|> shouldSolveType (TDef.Generalize (%0 ^-> %0))

(fun x -> x) "hello"

String

The companion to the generalization test: now that identity has the polytype forall a. a -> a, applying it to a string should pin a to String at this call. This is the first time we see the instantiation step at work — the generic a gets fixed from the argument type flowing in.

X.App (X.Fun (X.Ident "x") (X.Var "x")) (X.Lit "hello")
|> solve [] None
|> shouldSolveType (Mono BuiltinTypes.string)

(fun x -> x) 42

Number

Same instantiation trick, now with a number. Having the two cases side by side (String and Number) is the whole point — it shows that each application picks its own type for a independently, which is what polymorphism promises.

X.App (X.Fun (X.Ident "x") (X.Var "x")) (X.Lit 42)
|> solve [] None
|> shouldSolveType (Mono BuiltinTypes.number)

add : Number -> Number -> Number

add 100 10

Number

Arrows are right-associative: Number -> Number -> Number reads as Number -> (Number -> Number). So add takes a number and returns another function that takes a number and returns a number. Applying both arguments here therefore gives back a Number.

X.App (X.App (X.Var "add") (X.Lit 100)) (X.Lit 10)
|> solve
    [ "add", Mono (BuiltinTypes.number ^-> BuiltinTypes.number ^-> BuiltinTypes.number) ]
    None
|> shouldSolveType (Mono BuiltinTypes.number)

add : Number -> Number -> Number

add 100

Number -> Number

Partial application returns a function waiting for the remaining args.

X.App (X.Var "add") (X.Lit 100)
|> solve
    [ "add", Mono (BuiltinTypes.number ^-> BuiltinTypes.number ^-> BuiltinTypes.number) ]
    None
|> shouldSolveType (Mono (BuiltinTypes.number ^-> BuiltinTypes.number))

fun f x -> f x

forall a b. (a -> b) -> a -> b

The apply-combinator. A higher-order function is one that takes another function as an argument (or returns one) — here f is a parameter that gets applied to x. A combinator is just a self-contained function that refers only to its parameters (no outside names). From f x, the inferencer learns that f must accept whatever type x has and produce some return — so f : a -> b, with a and b both free. The whole expression generalizes over both.

X.Fun (X.Ident "f")
    (X.Fun (X.Ident "x")
        (X.App (X.Var "f") (X.Var "x")))
|> solve [] None
|> shouldSolveType (TDef.Generalize ((%0 ^-> %1) ^-> %0 ^-> %1))

fun f x -> f (f x)

forall a. (a -> a) -> a -> a

Feeding f x back into f forces input and output of f to have the same type — constraining to a -> a.

X.Fun (X.Ident "f")
    (X.Fun (X.Ident "x")
        (X.App (X.Var "f") (X.App (X.Var "f") (X.Var "x"))))
|> solve [] None
|> shouldSolveType (TDef.Generalize ((%0 ^-> %0) ^-> %0 ^-> %0))

add : Number -> Number -> Number

add 10 "hello"

Can't unify Number and String

"Unify" is type-checker jargon for "make these two types agree". When the inferencer meets add's signature (second arg: Number) and a string literal at that position, it tries to unify Number with String — and fails, because they're plainly different.

X.App (X.App (X.Var "add") (X.Lit 10)) (X.Lit "hello")
|> solve
    [ "add", Mono (BuiltinTypes.number ^-> BuiltinTypes.number ^-> BuiltinTypes.number) ]
    None
|> shouldFail