# Type¶

## Backlinks¶

- Type Theory
- Type theory is the study of types.

- A type has normal form
- In Pie a Type has a normal form just like any other expression would. A type is the same as another type if they share the same normal form.

- A type describes a set of possible values
- In type theory, a type describes a set of possible values. This is usually used to declare what is possible to exist within a variable.

- A type is the same as another type if they share a normal form
- In Pie, any two Types which share the same normal form are the same type. They are effectively isomorphic. Therefore

- The normal form of an expression is determined by the type of the expression
- Because the normal form of an expression has a constructor for a type on top, asking for the normal form of an expression without a Type is meaningless in Pie. It isn't possible to normalise anything without type information.