Why Invisible Types
Full type safety without type annotations.
The Insight
Most statically typed languages ask you to write types. Loon does not.
Not for lack of a type system. Loon has a full, sound one, with generics, algebraic data types, and effect tracking. You simply never write the types yourself. The compiler works them all out.
The reasoning runs deeper than convenience. Types exist to help the compiler catch your mistakes, not, at least not first, to help you express intent. So if the compiler can recover every type on its own, writing them by hand is ceremony: noise wedged between you and the logic you came to write.
Loon follows that idea to its conclusion. The compiler uses Hindley-Milner inference to determine the type of every expression in your program. You write code. The compiler checks it. When something fails to line up, you get a precise error. The types are present at all times, working behind the scenes, and you never have to spell a single one of them out.
How Hindley-Milner Inference Works
The intuition is plainer than the name. 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 required.
The same reasoning scales to your entire program. The compiler walks every expression, gathering constraints of the form "this must be the same type as that", then solves the whole set at once. If the constraints are satisfiable, the program type-checks. If they are not, the error points to exactly where the types collide.
Note
HM inference is neither heuristic nor best-effort. It is a complete algorithm: if a valid typing exists, it finds it; if none exists, it reports an error. There is no third outcome.
What Gets Inferred
Function signatures
Every parameter type, return type, and generic is inferred automatically. If a function happens to work on any type, the compiler notices and makes it polymorphic for you:
[fn identity [x] x]
; Inferred: forall a. a -> a
[fn first [pair]
[get pair 0]]
; Inferred: (a, b) -> aGenerics
You never write generic parameters. The compiler reads them off how the function is used. If a function applies its argument to both elements of a pair, the compiler concludes that argument is 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 learns its type from the constructors you name. Pattern matching is more than control flow; it is a rich source of type information:
[fn describe [opt]
[match opt
[Some x] [str "got: " x]
None "nothing"]]
; Inferred: Option Str -> StrEffects
Effect types are inferred too. If your function performs an effect, the compiler records it in the type without you ever declaring it. The type system therefore knows precisely which side effects each function can perform, and it worked that out entirely on its own:
[fn read-name []
[perform Console.readline "Name: "]]
; Inferred: () -> Str / ConsoleThe Editor as Type Viewer
If types never appear in the source, where do you see them? In your editor. The Loon language server offers three features that make the invisible vivid:
- Hover types: hover over any expression to see its inferred type.
- Inlay hints: faded type annotations shown inline, without touching your code.
- Error squiggles: type errors surface the instant you introduce them.
This is a better arrangement than writing types by hand. A hand-written annotation is a snapshot, and snapshots go stale as the code around them moves. An editor-provided type is always correct, because it comes straight from the compiler. You see types everywhere and pay nothing to keep them honest.
When You Might Want Annotations
For the rare moments when you do want to state a type outright, Loon offers the optional sig form:
[sig parse : Str -> Result Int ParseError]
[fn parse [input]
...]A few situations reward it. At a module boundary, a sig makes the public API contract explicit for anyone reading the code. To constrain polymorphism, a sig lets you make a function less general than the compiler would infer. And when a type error has you puzzled, a sig gives the compiler a fixed reference point and helps localize the conflict.
Tip
sig is always optional. The compiler checks your annotation against its own inference, and if the two disagree, you get an error.
Frequently Asked Questions
Is this like TypeScript's type inference?
Not quite. TypeScript infers types inside a function but expects annotations at its boundaries. Loon's inference is global. It crosses function boundaries freely, so you never annotate a parameter or a return type. The whole program is a single inference problem, and the compiler solves all of it at once.
What about documentation?
The usual case for annotations is that they document. We think the editor documents better, since its types are always accurate, and that good names do the rest. A function called parse-int tells you its purpose more clearly than fn parse_int(s: &str) -> Result
Does inference slow down compilation?
No. HM inference runs in nearly linear time on real programs. It is not a meaningful share of compile time, and Loon's compiler is fast enough that you will never feel it.
Can the inferred types be surprising?
Now and then 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 works on more inputs than you had in mind. To rein it in, add a sig.