Information Aware Type Systems and Telescopic Constraint Trees

TL;DR

Problem: how to model information flow in type systems and provide a general, constraint-based account of type checking and inference. Approach: develop Information Aware STLC with information effects and a constraint-based representation, plus Telescopic Constraint Trees that encode typechecking as a space-time tree; include mode analysis and a Hindley–Milner extension. Contributions: (i) a linear-by-default constraint discipline with explicit duplication, (ii) a CPS-like telescopic tree semantics that yields conventional checkers via unification, (iii) HM extension via StartM/StartP semantics, and (iv) discussion of debugging/elaboration and future work. Impact: provides a generalizable, debuggable framework for designing typecheckers and understanding data flow in programs.

Abstract

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 and help in implementing them. I also calculate a general, scoped, constraint-based representation of typechecking problems from the typing rules.

Figures (8)

• Figure 1: Constraints for STLC
• Figure 2: Information Aware Simply Typed Lambda Calculus
• Figure 3: Telescopic constraints
• Figure 4: STLC Telescopic Tree Semantics
• Figure 5: Telescopic Constraint Tree semantics for Annotated Lambda