Information Aware Type Systems andTelescopic Constraint Trees
Philippa Cowderoy

MSFP 2020

email:
twitter:

Philippa Cowderoy

flippa@flippac.org@flippac

Info Aware Type Systems and TCTs

MSFP 2020

1 / 41

What I’m Talking About

Motivating ‘information awareness’
Tools for information awarenessInformation Aware Type Systems

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

2 / 41

What I’m Talking About

Motivating ‘information awareness’
Tools for information awarenessInformation Aware Type Systems

Telescopic Constraint Trees

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

2 / 41

Information Awareness?
Some people find AppEq easier to read than AppTrad. Why?
Γ ` Tp : τ p
Γ ` Tp : τ p

Γ ` Tf : τ f

Γ ` Tf : τ p → τ r

τf = τp → τr

Γ ` Tf Tp : τ rAppTrad

Γ ` Tf Tp : τ r AppEq

AppEq shows us explicitly the information we infere.g. Tf is a function that can take Tp as a parameter

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

3 / 41

Information Aware Variable Use?

What does this τ say?

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

4 / 41

Information Aware Variable Use?

What does this τ say?

Using schematic variables can mean different things:
Does it use known information?
Is it a pattern?
Is it part of a non-linear pattern?
Can it be reduced first? (Should it?)

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

4 / 41

Part Way There

We want an ‘information aware’ approach
Let us be explicit about this!

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

5 / 41

Part Way There

We want an ‘information aware’ approach
Let us be explicit about this!

Constraints can help us do better. . .
. . . But they can’t stop us doing worse

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

5 / 41

What I’m Talking About Now

Motivating ‘information awareness’ – DONE
Tools for information awarenessInformation Effects
Constraints

Information Aware Type Systems
Telescopic Constraint Trees

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

6 / 41

Information Effects

From Information Effects by James & Sabry
Mostly-reversible programming

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

7 / 41

Information Effects

From Information Effects by James & Sabry
Mostly-reversible programming
Seen via isomorphic programming

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

7 / 41

Information Effects

From Information Effects by James & Sabry
Mostly-reversible programming
Seen via isomorphic programming

I can still use the idea in just one direction!

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

7 / 41

Information Effects Are. . .

Breaches of conservation of information:
When information is created
When information is destroyed

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

8 / 41

Information Effects Are. . .

Breaches of conservation of information:
When information is created
When information is destroyed
When information is duplicatedPhilippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

8 / 41

Information Effects Are. . .

Breaches of conservation of information:
When information is created
When information is destroyed
When information is duplicatedInference creates new information
Implied by the information we havePhilippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

8 / 41

Contraints as Information

SyntaxStatic Semantics
Dynamic Semantics

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

9 / 41

Contraints as Information
SyntaxJust what we wrote
Information as in bits
Bits are a bad unit for precise accounting!
Static Semantics
Dynamic Semantics

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

9 / 41

Contraints as Information
SyntaxStatic Semantics

What holds if the constraint is satisfied?
Satisfaction predicate
What shapes of problem are solveable?
Dynamic Semantics

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

9 / 41

Contraints as Information
SyntaxStatic Semantics
Dynamic Semantics

Part of a constraint problem
Part of the process of solving that problem

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

9 / 41

Contraints as Information
SyntaxStatic Semantics
Dynamic Semantics

Part of the process of solving a problem
A process that can block on unknown information. . . Or provide information
Unknowns represented bysolver variables or metavariables

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

9 / 41

Contraints as Information

SyntaxStatic Semantics
Dynamic Semantics
Insight

Constraints are a unit of information!

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

9 / 41

What I’m Talking About Now
Motivating ‘information awareness’ – DONE
Tools for information awareness – DONE
Information Aware Type Systems
AimMethods
Example – Simply Typed Lambda Calculus
Modes
Telescopic Constraint Trees
Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202010 / 41

Information Aware Type Systems – Aim

Clear introduction and elimination of information

Clear data flow

Clear choices about flow
In design and implementation

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202011 / 41

Information Aware Type Systems – Methods

Linear logic variables: one +ve source, one -ve sink
Constraints
Generation is an information effect
Keep dataflow general
Flexible abstraction
Explicit duplication

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202012 / 41

Constraints for the Simply Typed Lambda Calculus

τ =τx :τ ∈Γ0Γ := Γ ; x : τΓ−hΓΓType equality
Binding in context
Context extension
Context duplication

Convention: write L = R as if ‘assigning’ to L
Context constraints ⇒ structural rules

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202013 / 41

Information Aware Simply Typed λ-Calculus – Varτ =τx :τ ∈ΓΓ0 := Γ ; x : τΓ−hΓΓType equality
Binding in context
Context extension
Context duplication

x :τ ∈ΓΓ ` x : τ Var

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202014 / 41

Information Aware Simply Typed λ-Calculus – Lamτ =τx :τ ∈ΓΓ0 := Γ ; x : τΓ−hΓΓType equality
Binding in context
Context extension
Context duplication
Γf := Γ ; x : τ p
Γf ` T : τ r
τf = τp → τrΓ ` λx.T : τ f Lam

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202015 / 41

Information Aware Simply Typed λ-Calculus – Appτ =τ
x :τ ∈ΓΓ0 := Γ ; x : τΓ−hΓΓType equality
Binding in context
Context extension
Context duplication
Γ−hΓf
Γp

Γf ` Tf : τ f

Γp ` Tp : τ p

τp → τr = τf
Γ ` Tf Tp : τ rPhilippa Cowderoy

Info Aware Type Systems and TCTs

AppMSFP 202016 / 41ModesWhich way is data flowing?
When do we know enough to solve a constraint?

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202017 / 41ModesWhich way is data flowing?
When do we know enough to solve a constraint?

Data flows +ve to -ve
Constraints can ‘fire’ when -ve variables known

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202017 / 41

Different Modes of a Type SystemModeΓ+ ` T + : τ +Γ+ ` T + : τ −Γ− ` T + : τ +Γ− ` T + : τ −Γ+ ` T − : τ +Unidirectional
Type checking
Free variabletypes
Proof search
Programsynthesis

Bidirectional
Checking
Synthesis
Checked type
Synthesised type

Each mode can have its own implementation(‘procedure’)
Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202018 / 41

→ - The Other Information Effect

The function arrow → doesn’t appear in source
It does appear in our types

Information we infer from or create about terms

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202019 / 41

Moding →I assign two different modes to →:Based on how the solver handles = constraints
LHS of = is being ‘assigned to’ in some form+ve construction vs -ve pattern-matching

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

20 / 41

Information Aware Simply Typed λ-Calculus (moded)
Var
Mode: Γ+ ` T + : τ − (Synthesis or ‘typechecking’)x − : τ + ∈ Γ−Γ+ ` x + : τ − Var

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202021 / 41

Information Aware Simply Typed λ-Calculus (moded)
Lam
Mode: Γ+ ` T + : τ − (Synthesis or ‘typechecking’)Γf + := Γ− ; x − : τ p +Γf − ` T − : τ r +τ f + = τ p − →+ τ r −Γ+ ` λx + .T + : τ f − Lam

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202022 / 41

Information Aware Simply Typed λ-Calculus (moded)
AppMode: Γ+ ` T + : τ − (Synthesis or ‘typechecking’)+ΓfΓ− −hΓp+Γf − ` Tf − : τ f +Γp − ` Tp − : τ p +τ p − →− τ r + = τ f −Γ+ ` Tf + Tp + : τ r −Philippa Cowderoy

Info Aware Type Systems and TCTs

AppMSFP 202023 / 41

Information Aware Simply Typed λ-CalculusΓf := Γ ; x : τ p
Γf ` T : τ rx :τ ∈Γτf = τp → τr

Γ ` x : τ VarΓ ` λx.T : τ f Lam
Γ−hΓf
Γp

Γf ` Tf : τ fΓp ` Tp : τ pτp → τr = τfΓ ` Tf Tp : τ rPhilippa Cowderoy

Info Aware Type Systems and TCTs

AppMSFP 202024 / 41

What I’m Talking About Now

Motivating ‘information awareness’ – DONE
Tools for information awareness – DONE
Information Aware Type Systems – DONE
Telescopic Constraint Trees
What they are and do
How to build themThings to do with them!

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202025 / 41

What’s a Telescopic Constraint Tree?

A Telescopic Constraint Tree (or TCT) is:
A Tree – a refined AST
Containing Constraints
Telescopic

Philippa CowderoyInfo Aware Type Systems and TCTs

MSFP 2020

26 / 41

What’s a Telescopic Constraint Tree?

A Telescopic Constraint Tree (or TCT) is:
A Tree – a refined AST
Containing Constraints
Also metavariable binders
Telescopic

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

26 / 41

What’s a Telescopic Constraint Tree?

A Telescopic Constraint Tree (or TCT) is:
A Tree – a refined AST
Containing Constraints
Also metavariable binders
Telescopic
Built from composable contexts

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

26 / 41

What Else is a Telescopic Constraint Tree?

A typechecking problem in progress
GenericDerivable from Information Aware Type Systems
A scope-aware constraint store

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202027 / 41

What Else is a Telescopic Constraint Tree?

A typechecking problem in progress
Generic
Derivable from Information Aware Type Systems
A scope-aware constraint store
Scoping not needed for STLC
Useful for HM, dependent types and more!

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202027 / 41

What Does a Telescopic Constraint Tree Do?

What an ordinary typechecker doesPhilippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202028 / 41

What Does a Telescopic Constraint Tree Do?

What an ordinary typechecker does in time

Telescopic constraint trees do in space

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202028 / 41

Context Constraints In, um, Context?

We use these constraints, which refer to contexts:

x : τ ∈ Γ Binding in context
Γ := Γ ; x : τ Context extension
0We can’t put those directly in a telescope:
They want to refer to it!

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202029 / 41

Situated Constraints
Old Newx : τ ∈ Γ ?x : τ
Γ0 := Γ ; x : τ !x : τThe new constraints are situated.
Their meaning depends on their position in the telescope:
Description?x : τ Query/Ask for current binding [here]!x : τ Generate/Tell about binding [here]
Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202030 / 41

Binding and Equalityτ = τ Type equality constraint∃τ Bind an unknown τ∃τ =τ Bind τ with current solution

We can ask “is this solved?”

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202031 / 41

The Easy One

Context duplications are tree branches!

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202032 / 41

Building Trees

We build a TCT by traversing the ASTA ‘TCT semantics’: JT K τ
Translate T into a TCT
Have τ become the result type

Retaining all information from the typing rules!

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202033 / 41

Starting the Build

Suppose we want to synthesise a type:
Γ+ ` T + : τ −We use this rule to build this tree:
Γ+ , {∃τ − }, JT + K τ +(Start)

τ acts as a query variable

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202034 / 41

Building Var

This typing rule:
x :τ ∈ΓΓ ` x : τ Var
Becomes this TCT rule:Jx + K τ − = {?x − : τ + }Philippa Cowderoy

Info Aware Type Systems and TCTs

(Var )MSFP 202035 / 41

Building Lam
Γf := Γ ; x : τ p +Γf ` T : τ r +τ f = τ p− → τ r −Γ ` λx.T : τ f

Lam

Jλx.T K τ f ={∃τ p, ∃τ r , τ f = τ p − → τ r − , !x : τ p + }, JT K τ r + (Lam)
Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202036 / 41

Building AppΓ−hΓfΓpΓf ` Tf : τ f

Γp ` Tp : τ p

τp → τr = τf
Γ ` Tf Tp : τ r

AppJTf TpK τ r ={∃τ f , ∃τ p, τ p → τ r = τ f } | JTf K τ f| JTpK τ p (App)Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

37 / 41

What can I do with them?

We can, of course, implement typecheckers.
We can also instrument those checkers:
Changes in the tree show the process, including scope
Those changes preserve the AST structure
Mostly – labels are useful extra info
UI for type level debugging?

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

38 / 41

What else can I do with them?
We can usually fuse TCTs away:
Assuming we have:
A greedySolver for the TCT’s constraints
A treeGenerator , implementing JT K τ
We can pick treeGenerator ’s traversal strategy
And fuse greedySolver ◦ treeGenerator
Exceptions are interesting! Greed doesn’t always work.
Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202039 / 41

What else can I do with them?

We can find and explain optimisations:
For HM:(not my trick! – MLton?)
Generalisation depth – generalisation constraints from root
Annotate every ∃τ with its generalisation depth
Constraints generalise variables at their depth
Generalisation is now linear in type size

Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 202040 / 41

If you remember one thing. . .
Telescopic Constraint Trees do in space
what conventional checkers do in time
Some extras:
Information effects track information well
Constraints are a unit of information
Information Aware Type Systems
Telescopic Constraint Trees can be derived
We can calculate, trade off and optimise from TCTs
Philippa Cowderoy

Info Aware Type Systems and TCTs

MSFP 2020

41 / 41