Little typer
- Normal forms
- Sameness according to a type
- 2 values the same <-> same normal form
- values the same if same constructor applied to the same values
- expression with constructor at top -> value
- constructors are the direct way of constructing expressions of that type
- value enough because the top-level ctor will dictate what happens next
- eliminators take apart values created by data constructors
- lambda is data ctor for functions
- function application is the eliminator for functions
- Two )-expressions that expect the same number of ar- guments are the same if their bodies are the same after consistently renaming their variables.
- neutral values - cannot be evaluated, nor are they values
- identical neutral values are the same
- U as a type constructor?? maybe because it describes type expressions??
- type expressions describe expressions
- U describes all types
- type of a type is U
- a type constructor is not a type expression
- Pair A D is a type when A and D are types
- not every type is described by U
- Pear definition