Expand description
Types and Type Inference
Every Simplicity expression has two types associated with it: a source and a target. We refer to this pair of types as an “arrow”. The types are inferred from the structure of the program.
Simplicity types are one of three things
- A unit type, which has one value
- A sum of two other types
- A product of two other types
During type inference, types are initially “free”, meaning that there are
no constraints on what they will eventually be. The program structure then
imposes additional constraints (for example, the comp combinator requires
that its left child’s target type be the same as its right child’s source
type), and by unifying all these constraints, all types can be inferred.
Type inference is done progressively during construction of Simplicity
expressions. It is completed by the Type::finalize method, which
recursively completes types by setting any remaining free variables to unit.
If any type constraints are incompatible with each other (e.g. a type is
bound to be both a product and a sum type) then inference fails at that point
by returning an error.
In addition to completing types Type::finalize, does one additional
check, the “occurs check”, to ensures that there are no infinitely-sized
types. Such types occur when a type has itself as a child, are illegal in
Simplicity, and could not be represented by our data structures.
Modules§
- arrow
- Types Arrows
Structs§
- Bound
Ref - Context
- Type inference context, or handle to a context.
- Final
- Data related to a finalized type, which can be extracted from a
super::Typeif (and only if) it is finalized. - Type
- Source or target type of a Simplicity expression.
Enums§
- Complete
Bound - A finalized type bound, whose tree is accessible without any mutex locking
- Error
- Error type for simplicity