Information Aware Type Systems andTelescopic Constraint Trees
Philippa Cowderoy
flippa@flippac.org

Can we use the flow of information to understand type systems? I present two familiar type systems in pursuit of an ‘Information Aware’ style, using information effects to reveal data flow andhelp in implementing them. I also calculate a general, scoped, constraint-based representation oftypechecking problems from the typing rules.

1Introduction and BackgroundHow does information arise and flow in type systems?
I will attempt to answer this by presenting type systems in an ‘Information Aware’ style, making
heavy use of information effects [4] which first arose in reversible programming. The paper introduces
a combinator language for ‘isomorphic programming’ in the same sense as functional programming. Information effects show where, in an otherwise isomorphic program, information is created or destroyed.
In an interpreter or semantics, the created information is the meaning of the input program. Correspondingly, in a type system information effects help to keep track of meaning and how it relates to theflow of information. By following the origin and flow of information we can derive algorithms, gain
intuitions about algorithmic behaviour, and abstract away implementation details. Here I apply this totype checking and inference.
I also use constraints as a critical abstraction. Firstly they act as a unit of information. They also haveboth static and dynamic semantics: satisfaction predicates state when a constraint is satisfied, separatelyfrom when or how constraints can be solved.
Describing type systems using constraints is constraint logic programming. Such programs often
won’t correspond to a single isomorphic program – instead, procedures implementing them for specificmodes do [6] [7]. Typings of known source terms are programs, generating constraint problems.

2Information Aware Simply Typed Lambda Calculus

The type system in figure 2 uses constraints shown in figure 1.
The system itself is a presentation of the conventional simply
typed lambda calculus without type annotations.
Due to the discipline imposed by information effects,
metavariables are linear: used at one source and one sink. Duplication must be explicit as it creates copies of information. Constraint generation also creates information, as does constructing
the function arrow – something which we are inferring from thesource.

Submitted to:
MSFP 2020τ =ττ−hττx:τ ∈Γ
Γ := Γ ; x : τΓ−hΓΓType equality
Type duplication
Binding in context
Context extension
Context duplication

Figure 1: Constraints for STLC

2Information Aware Type Systems

To truly explain the semantics of a typed lambda calculus, we need not just the types but the semanticsof the context – including the structural rules, encoded into the semantics of the context constraints.
These can even be altered to produce a minimal substructural system.
The system supports any modes a solver is available for – though proof search remains hard! Examples can be found in appendix A. Supporting annotations requires type duplication – see appendix B fordetails.

x:τ ∈Γ

Γ f := Γ ; x : τ p
Γ f ` T : τr
τ f = τ p → τr

Γ ` x : τ VarΓ ` λ x.T : τ f Lam

Γ−hΓΓpf
Γf ` Tf : τ f
Γp ` Tp : τ p
τ p → τr = τ f
Γ ` T f Tp : τr

AppFigure 2: Information Aware Simply Typed Lambda Calculus
The Var rule asserts that the binding x : τ is in the context Γ. Lam uses a context extension to relate
the context of the lambda to that of its body, with an equality constraint spelling out the relationshipbetween the parameter type, the body type and the function represented by the lambda. App duplicatesits context in order to type its subterms and the equality constraint relates function, parameter and result.
Below is a mode analysis for type system used at the mode Γ+ ` T + : τ − , aka type synthesis or‘typechecking’. It’s a worthwhile exercise to connect each +ve variable to its -ve counterpart: constraints
can fire when all their -ve inputs are available, producing +ve outputs (possibly unknown!) and showing
the flow of data.
Γ f + := Γ− ; x− : τ p+
Γ f − ` T − : τr++

Γ− −hΓΓpf +Γf− ` T f− : τ f+

Γp− ` T p− : τ p+x− : τ + ∈ Γ−

τ f + = τ p− →+ τr−τ p− →− τr+ = τ f −Γ+ ` x+ : τ − VarΓ+ ` λ x+ .T + : τ f − LamΓ+ ` T f + Tp+ : τr−3App

Telescopic Constraint Trees

A telescopic constraint tree is a refinement of the AST
into a de Bruijn telescope extended with branching∃τ Bind an unknown τ(represented here using |) and scoped constraint ma- ∃τ=τ Bind τ with current solutionchinery. The tree traces in space where a traditional?x : τ Query/Ask for current binding [here]checker will go over time. This provides a general!x : τ Generate/Tell about binding [here]
representation of typechecking problems.
Figure 3: Telescopic constraints
Figure 4 contains a CPS-like transformation using the quantifiers and constraints in figure 3. It begins with the Start rule, filling in T and what is known about Γ and τ. Constraint contexts are translated
into branches for −h or ‘situated’ constraints that do not mention their context. Instead, their semantics
depend on their position in the tree structure: !x : τ requires a binding at that exact location and thebehaviour of ?x : τ depends on the bindings in its scope.

Philippa CowderoyJxKJλ x.T K
JT f TpKrrr===3Γ, {∃τ}{?x : r}{∃τ p, ∃τr, r = τ p → τr, !x : τ p}{∃τ f , ∃τ p, τ p → r = τ f },JT K τ,||JT K τrJT f K τ f
JTpK τ p(Start)
(Var)
(Lam)
(App)

Figure 4: STLC Telescopic Tree Semantics
Given the translation between the two styles of context constraint and branching, the rules in figure 2and figure 4 can each be derived from the other in a mechanical fashion. Insofar as any typechecker canbe explained in terms of the typing rules it can be explained at least as well in terms of the tree.
As an example, here is the tree for (λ x.x) y in an empty context:{}, {∃τ}, {∃τ f , ∃τ p, τ p → τ = τ f } |{∃τ p0 , ∃τr, τ f = τ p0 → τr, !x : τ p0 }, {?x : τr}|{?y : τ p}
With simple types, it is safe to lift the quantifiers to the root of the tree followed by the non-context
constraints. Solving the situated context constraints leaves the traditional logical semantics of an unscoped constraint store, followed by context data. A conventional checker can now be recovered byfusing all these processes and solving equality constraints with unification as they arise.
By making use of the scoped metavariables and additional situated constraints the techniques inGundry et al. [2] can readily be adapted to implement Hindley-Milner inference as well – see appendix
C. This constraint-based formulation also owes much to Bastiaan Heeren [3], while Gundry’s thesis [1]shows how to extend the techniques to a dependently typed setting.

4

Related & Future Work

Discussion of solving −h at various modes in a linear system recently proved helpful to McBride [5].
Elaboration problems are worth exploring: they often involve destroying information due to syntactic sugar, and the reversible nature of information effects’ original setting may prove useful as well.
Documenting where information is destroyed in one direction also shows where it could be ‘recreated’
from logs to reverse the process. Careful tracking of constraints may also help show that if the elaborator
succeeds, so does target typechecking. Edwin Brady and I plan to try this using the core of Idris.
More generally I would like to explore using telescopic constraint trees to help in debugging typeerrors, distinguishing where constraints are unsolveable due to lack of information from where they are
known unsatisfiable. Ultimately I hope to help users trace the flow of failure to its source(s).

5Conclusion

While the type systems presented here are simple and familiar, the presentation itself offers real advantages. The linear-by-default discipline enforced by information effects allows the information aware
style to shed light on questions about data and information flow.
The ease with which telescopic constraint trees are derived from information aware systems is backedby – even at this informal level – a high degree of confidence that they are a truly general representationof typechecking problems. Put simply, they retain the information in an information aware typing. Thiscan then be used to calculate a typechecker with desired properties.

4Information Aware Type SystemsReferences[1] Adam Gundry (2013): Type Inference, Haskell and Dependent Types. Ph.D. thesis, University of Strathclyde.
Available at http://adam.gundry.co.uk/pub/thesis/.
[2] Adam Gundry, Conor Mcbride & James McKinna (2010): Type inference in context. In: MSFP ’10 Proceedings of the third ACM SIGPLAN workshop on Mathematically structured functional programming, pp. 43–54,
doi:10.1145/1863597.1863608.
[3] Bastiaan J. Heeren (2005): Top Quality Type Error Messages. Ph.D. thesis, Universiteit Utrecht, The Netherlands. Available at http://www.cs.uu.nl/people/bastiaan/phdthesis.
[4] Roshan P. James & Amr Sabry (2012): Information effects. In John Field & Michael Hicks, editors: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012,
Philadelphia, Pennsylvania, USA, January 22-28, 2012, ACM, pp. 73–84, doi:10.1145/2103656.2103667.
Available at https://doi.org/10.1145/2103656.2103667.
[5] Conor McBride (2018): Everybody’s Got To Be Somewhere. doi:10.4204/EPTCS.275.6.
[6] Uday S. Reddy (1993): A typed foundation for directional logic programming. In: Extensions of LogicProgramming, Springer Berlin Heidelberg, pp. 282–318, doi:10.1007/3-540-56454-3 15. Available at https://doi.org/10.1007/3-540-56454-3_15.
[7] Ekkehard Rohwedder & Frank Pfenning (1996): Mode and termination checking for higher-order logic programs. In: Programming Languages and Systems — ESOP '96, Springer Berlin Heidelberg, pp. 296–310,
doi:10.1007/3-540-61055-3 44. Available at https://doi.org/10.1007/3-540-61055-3_44.

AIASTLC Modes

Here are some examples of modes the rules in figure 2 can be used in, and common ways of describing
them. The ‘Unidirectional’ column covers descriptions that ignore the difference between checking andsynthesis, while the ‘Bidirectional’ column adds that detail.
ModeUnidirectional

BidirectionalΓ+ ` T + : τ +Type CheckingChecking

Γ+ ` T + : τ −Γ− ` T + : τ +Synthesis, Inference
Free Variable Analysis

Γ− ` T + : τ −Γ+ ` T − : τ +with checked types
with synthesised types

Proof Search, Program Synthesis

Philippa Cowderoy

B

5Annotations

Annotations are redundant in STLC, and it requires type duplications tohandle them. The preferable approach is to duplicate the annotation, pushτa−hτapτa fing one copy in to ‘check’ and returning the other as if ‘synthesised’.
Γ f := Γ ; x : τap
There are alternative ways to write the rule. Sadly information effectsΓ f ` T : τr
do not go so far as to force the reinvention of bidirectional typechecking.
τ f = τa f →τr
The only requirement is that the annotation is consistent with both the Γ ` λ x : τa . T : τ f ALamcontext of the lambda’s body and the resulting function type. This could
also be achieved by modifying Lam to duplicate τ p or even τ f and checkthat against the annotation, making it less clear that a partial result can be returned immediately.
Jλ x : τa . T Kr={∃τap, ∃τa f , τa−hτapτa f , !x : τap, r = τa f →τr}

,JT K τr(ALam)

Figure 5: Telescopic Constraint Tree semantics for Annotated Lambda

CHindley-Milner

Figure 7 contains typing rules for a system in the vein of Hindley-Milner, while figure 8 gives a corresponding telescopic constraint tree semantics (use StartM for monomorphic results, StartP for polymorphic). Both use the constraints in figure 6.
For consistency, this presentation uses n-ary polytypes σ ::= ∀ā.τ. For n = 0, we have ∀.τ isomorphicto τ, leaving the App and Lam rules isomorphic to STLC’s – the hallmark of rank-1 polymorphism. Allbindings are of the form x : σ . This means the context doesn’t tell us which variables are let-bound, but
simplifies instantiation.
Where as Gundry et al. [2] use # as a separator, I have chosen to pair <Gen> with </Gen>. Duringsolving, the two delimit the quantifiers to be generalised and </Gen> does the actual generalisation. I
have also written Γ−h{Γ̄} as sugar for n-ary context duplication.
∃σ∃σ =τx:σ ∈ΓΓ := Γ ; x : σ?x : σ!x : σσ ≥τ
σ = GenΓ (τ)<Gen></Gen (σ ≥ τ)>

Bind an unknown σ
Bind σ with current solution
Binding in context
Context extension
Query/Ask for current binding [here]
Generate/Tell about binding [here]τ is an instance of σσ generalises τ in Γ
Begin generalisation region/‘separator’End region/generalise τ into σ
Figure 6: Hindley-Milner constraints

6Information Aware Type Systems

Γ−hΓΓpf
Γf ` Tf : τ f
Γp ` Tp : τ p
τ p → τr = τ f

Γ f := Γ ; x : ∀.τ p
Γ f ` T : τr
τ f = τ p → τrΓ ` λ x.T : τ f

Γ ` T f Tp : τrLamAppΓ−h{ΓB, Γgen, ΓT }
ΓB ` T b : τb
σ = GenΓgen (τb)
ΓT 0 := ΓT ; x : σ
ΓT 0 ` T t : τx:σ ∈Γσ ≥τΓ ` x : τ VarΓ ` let x = T b in T t : τ Let

Figure 7: Information Aware Hindley-Milner rules

JxK
Jλ x.T KJT f T pKrrr===

Jlet x = T b in T tK

Γ, {∃τ}Γ, {∃σ , <Gen>, ∃τ, </Gen (σ ≥ τ)>}{∃σ , ?x : σ , σ ≥r}{∃τ p, ∃τr, r = τ p → τr, !x : τ p}{∃τ f , ∃τ p, τ p → r = τ f }
r

=

{∃σ }

||,,JT K τJT K τ(StartM)(StartP)
(Var)
(Lam)
(App)

, JT K τr| JT f K τ f| JT pK τ p{<Gen>, ∃τ, </Gen (σ ≥ τ)>}, JT bK τ{!x : σ }, JT tK τr

Figure 8: Hindley-Milner Telescopic Tree Semantics(Let)