Many statically typed languages perform type inference to varying degrees, and Pikelet is no different! The goal is to reduce the burden of writing type annotations everywhere. Some languages like OCaml and Elm can even infer the types of a whole program without any annotations at all!

Pikelet's type inference follows some very simple rules that you can probably pick up on your own, but we thought it might help to give a deeper explanation of how it works, without getting too bogged down in the theoretical details.

• Bidirectional type checking
  • Inferable terms
  • Checkable terms
• Further reading

Pikelet has a rather flexible type system that can have expressions embedded in them, so we've opted to use an algorithm known as 'bidirectional type checking' as a way to get a decent amount of inference while still remaining relatively predictable to you, the programmer. This means that you may sometimes have to write annotations on top-level definitions, but the types should propagate downwards and inner definitions should not require much annotation at all.

To do this we break the terms of the language into two groups. We call these inferable terms and checkable terms.

Inferable terms can be checked on their own or based on previous definitions.

TODO: Explain examples

Pikelet> true
Pikelet> "1"
Pikelet> 'a'
Pikelet> Bool
Pikelet> Type
Pikelet> Type^2
Pikelet> record { name = "Jane" }
Pikelet> Record { name : String }
Pikelet> record { x = 3.0 : F32; y = 3.0 : F32 }
Pikelet> \x : Int => x
Pikelet> (a : Type) -> a

Checkable terms need extra annotations, or be used in a position where extra information can be supplied.

TODO: Explain examples

Pikelet> 1
Pikelet> 2.0
Pikelet> record { x = 3.0; y = 3.0 }
Pikelet> \x => x

Pikelet> 1 : S32
Pikelet> 2.0 : F32
Pikelet> record { x = 3.0; y = 3.0 } : Record { x : F32; y : F32 }
Pikelet> \x => x : S32 -> S32

We describe Pikelet's type checking algorithm more formally in the appendix. If you have a background in programming languages and type theory this might be of interest to you. If not, that's ok - understanding the formal notation is not necessary for developing a high level intuition of type inference in Pikelet.