Little Typer
An introduction to dependent types, demonstrating the most beautiful aspects, one step at a time.
A program''s type describes its behavior. Dependent types are a first-class part of a language, and are much more powerful than other kinds of types; using just one language for types and programs allows program descriptions to be as powerful as the programs they describe. The Little Typer explains dep...
An introduction to dependent types, demonstrating the most beautiful aspects, one step at a time.
A program''s type describes its behavior. Dependent types are a first-class part of a language, and are much more powerful than other kinds of types; using just one language for types and programs allows program descriptions to be as powerful as the programs they describe. The Little Typer explains dep...
