Why Invisible Types

Full type safety without type annotations.

The Insight

Most statically typed languages ask you to write types. Loon does not.

This is not because Loon lacks a type system. It has a full, sound type system with generics, algebraic data types, and effect tracking. You just never write the types yourself. The compiler figures them all out.

The reasoning is simple: types exist to help the compiler catch your mistakes. They do not exist to help you express intent, at least not primarily. If the compiler can figure out every type on its own, then writing them by hand is ceremony. It is noise that sits between you and the logic you actually care about.

Loon takes this idea all the way. The compiler uses Hindley-Milner inference to determine the type of every expression in your program. You write code. The compiler checks it. If something does not line up, you get a clear error. The types are always there, working behind the scenes. You just never have to spell them out.

How Hindley-Milner Inference Works

The intuition is more straightforward than the name suggests. When you write:

[fn add [a b]
  [+ a b]]

The compiler sees + applied to a and b. It knows + takes two numbers and returns a number. So a and b must be numbers, and add returns a number. No annotation needed.

This process scales to your entire program. The compiler walks through every expression, generating constraints like "this must be the same type as that", then solves all the constraints at once. If they are satisfiable, the program type-checks. If they are not, you get an error pointing to exactly where the types conflict.

HM inference is not heuristic or best-effort. It is a complete algorithm. If a valid typing exists, it will find it. If no valid typing exists, it will report an error.

What Gets Inferred

Function signatures

Every parameter type, return type, and generic is inferred automatically. If a function works on any type, the compiler figures that out too and makes it polymorphic:

[fn identity [x] x]
; Inferred: forall a. a -> a

[fn first [pair]
  [get pair 0]]
; Inferred: (a, b) -> a

Generics

You never write generic parameters. The compiler infers them from how the function is used. If a function applies its argument to both elements of a pair, the compiler knows it needs a function from one type to another:

[fn map-pair [f pair]
  #[[f [get pair 0]] [f [get pair 1]]]]
; Inferred: forall a b. (a -> b) -> (a, a) -> (b, b)

ADTs and pattern matching

When you match on a value, the compiler knows its type from the constructors you use. Pattern matching is not just control flow; it is also a rich source of type information:

[fn describe [opt]
  [match opt
    [Some x] [str "got: " x]
    None     "nothing"]]
; Inferred: Option Str -> Str

Effects

Effect types are inferred as well. If your function performs an effect, the compiler tracks that in the type without you ever declaring it. This means the type system knows exactly what side effects each function can perform, and it figured it all out on its own:

[fn read-name []
  [perform Console.readline "Name: "]]
; Inferred: () -> Str / Console

The Editor as Type Viewer

If types are invisible in source code, where do you actually see them? In your editor. The Loon language server provides three features that make invisible types feel very visible:

  • Hover types: hover over any expression to see its inferred type.
  • Inlay hints: faded type annotations displayed inline, without editing your code.
  • Error squiggles: type errors appear instantly as you type.

This turns out to be a better workflow than writing types by hand. Hand-written annotations are static and can go stale as code evolves. Editor-provided types are always correct, because they come directly from the compiler. You get the benefit of seeing types everywhere without the cost of maintaining them yourself.

When You Might Want Annotations

Loon provides an optional sig form for the rare cases where you want to declare a type explicitly:

[sig parse : Str -> Result Int ParseError]
[fn parse [input]
  ...]

There are a few situations where this is helpful. At module boundaries, a sig makes the public API contract explicit for anyone reading the code. When you want to constrain polymorphism, a sig lets you make a function less general than the compiler would infer. And when you are debugging a confusing type error, adding a sig can help localize the problem by giving the compiler a reference point.

sig is always optional. The compiler checks that your annotation matches its inference. If they disagree, you get an error.

Frequently Asked Questions

Is this like TypeScript's type inference?

Not quite. TypeScript infers types within a function, but requires annotations at function boundaries. Loon's inference is global. It crosses function boundaries freely, so you never need to annotate a function parameter or return type. The whole program is one big inference problem, and the compiler solves it.

What about documentation?

The common argument for type annotations is that they serve as documentation. We think this is better solved by the editor, where types are always accurate, and by good naming. A function called parse-int communicates its purpose more clearly than fn parse_int(s: &str) -> Result does. The name tells you what it does; the types tell you the mechanical details. Let the editor handle the mechanical part.

Does inference slow down compilation?

No. HM inference runs in nearly linear time for practical programs. It is not a significant factor in compile times, and Loon's compiler is fast enough that you should not notice it at all.

Can the inferred types be surprising?

Occasionally, the compiler infers a more general type than you expected. This is always safe, because a more general type is strictly more permissive. Your function just happens to work on more inputs than you realized. If you want to constrain it, add a sig.