2024-08-22 • Prelim review - type-checking and inference

Recursive types

data NatList = Nil | Cons Nat NatList
 ↓
NatList = µX. <nil:Unit, cons:{Nat, X}>

Uses:

• Stream = µA. Unit -> {Nat, A}; Process = µA. Nat -> {Nat, A} takes current state as input.
• ClassWithSelf = µSelf. {get:Nat, inc:Unit -> Self}; defn with fix
• Well-typed (but diverging) fix.

What’s the relationship between NatList and <nil:Unit, cons:{Nat, NatList}>?

• Equi-recursive: definitionally equal. Conceptually simpler but bounded quantification and type operators are undecidable.
• Iso-recursive: isomorphic, but requires fold [T] (<...> -> T) and unfold [T] (NatList -> <...> with X -> T) operators. Can be inferred in practice, as it is in ML.

See TAPL §20, 2024-07-03 • denotational semantics and fancy types.

Type inference

Does there exist a type substitution from type variables to types such that ?

Our core algorithm has two parts.

• Constraint-based typing: during type-checking collect constraints on “these types must be equal” and only solve this after.
  • : has type whenever the constraint set is satisfied. is set of type variables introduced in rule, used to avoid overlapping variables.
  • e.g.,

• Unification: an algorithm to solve constraints by finding principal unifier.
  • Principal unifier = valid type substitution that makes the least amount of assumptions possible. All other substitutions can be recovered from this one by adding more stuff.
  • is trivial.
  • or adds the substitution ,
  • requires unifying and .
  • Anything else = fail.
  • The principal type of a term is the type of a term under the principal unifier.
• A type with variables is a type scheme (aka polytype), representing structure of type wrt universally quantified holes.
  • Do this to avoid type-checking entire type of let-bound variables on every occurrence.

Common pitfalls:

• Make sure you type-check unused let-bindings!
  • Let-polymorphism: let bindings can have polymorphic (i.e., generic) types, instantiated with specific types at each use site.
  • The naive way to do this with our constraint setup doesn't check binding type:

- Modify to ensure we type-check the binding, even if it isn't used:

• Let bindings and side effects can fuck things up
  • Since we infer the most general type for a let binding, every use might instantiate it differently.
  • ==Instantiating a read and write of Ref with different types is fucked==
  • Value restriction: let-binding is only polymorphic if not binding to a ref.

See TAPL §22, 2024-07-03 • denotational semantics and fancy types, semantic analysis.

Generics (parametric polymorphism) with System F

System F introduces universally quantified types , introduced at the term level with type abstractions and eliminated with type application . Contexts can bind type variables now too: . This is type-term abstraction.

• Above is type-passing semantics; we can also have type-erasure semantics: erase types, then evaluate
  • Results in different semantics: let f = (λX. error) in 0; != let f = error in 0;
• Polymorphism restricts definition: yields one possible function.
• A definition is impredicative if quantified variable could also include itself.
  • ; maybe !

See TAPL §23, 2024-07-03 • denotational semantics and fancy types, semantic analysis.

Inference

• In general, type inference is undecidable with full System F.
  • You can solve this by limiting where polymorphism happens (let-polymorphism, rank-2 polymorphism means no )
• Hindley-Milner type systems give you both quantification and inference by enforcing let-polymorphism.
  • Let-bindings are always polytypes with universal quantification.
    • Polytypes are stored as type schemes, with holes where quantified variables go.
  • Expressions are monotypes with no quantification.
    • Upon use, a polytyped expression has its holes replaced with fresh type vars.
    • When bound, a monotyped expression has its type inferred, then type variables are replaced with holes.

See Instantiation and generalization, TAPL §22.

Existentials

: inhabitant element of this type is value of type . Use this for ADTs, where is representation type, and is type of the record of class functions.

See TAPL §24.

Dependent types

λLF

• Types can depend on values:
  • Additionally, we have kinds, the type of types. Type families:
  • lambdas introduce pi types.
• Since types can be evaluated now, we need equivalence
  • Definitional equality: only include basic equalities that are obvious.
  • To actually implement this, convert to weak-head normal form (only beta-reduce head), check equivalence on WHNFs.
• A dependent sum type generalizes ordinary product types: can appear in .
• In Curry-Howard, dependent types get us from constructive, intuitionistic, or propositional logic to first-order logic, which has universal quantification.
  • A proof of has type

Calculus of constructions

Introduce functions from types to types. We have , representing propositions and “datatypes” like Nats, and , an inhabitant of a . Types as terms!

We introduce with all x:T. t. .

This is a pretty low-level representation of things. The calculus of inductive constructions gives us inductive (algebraic) data types.

Lambda cube

Three axes:

• Terms to types (type families)
• Types to terms (polymorphism)
• Types to types (type operators)

System	Term to term	Type families	Polymorphism	Type operators
	✓
	✓	✓
	✓		✓
	✓		✓	✓
	✓	✓	✓	✓

Link to original

A pure type system is a structure for doing typing of STLC-based languages with different kinds of abstractions. In a PTS, we have two sorts: proper types and kinds . Typing and kinding use the same operator (). Our terms also include all possible type expressions: abstractions, dependent products, etc. Our rules for the type/kind of the dependent product term is generic to a choice of input/output sort. Based on what we choose, we can recover all the kinds of abstractions listed above.

See 2024-07-24 • dependent & effect types (ATAPL 2: Dependent types).

Effect types

• means “Under , evaluating produces effect , yielding a value.”
  • Effect types: . Lazy language: “evaluating this produces .”
• Example: region-based memory management
  • Allocate values into different regions/arenas.
  • is set of regions that are accessed. Typing produces constraints on .
    • Introduction:

	- Elimination:

	- Lexically scoped regions aren't visible outside scope:

• To achieve deallocation of lexically scoped regions:

-

	- $\bullet$ is deallocated region.

• We can add effect polymorphism too. Allows us to not lock in specific selection of for functions like map.

• Can do region inference, generalizing as much as possible, building type tree, adding lexically scoped regions to remove them from from the outside world.

See 2024-07-24 • dependent & effect types (ATAPL 3: Effect types and region-based memory management).