References

<!-- Well, these references seem quite useful. Thanks! -->

This file contains a variety of useful references for those wanting to understand the concepts and research that underlie Enso's type system and type theory.

Intersection Types

• Taming the Merge Operator

Gradual Typing

• Approximate Normalisation for Gradual Dependent Types
• Gradual Type Theory
• Gradual Type-and-Effect Systems

Maximum Inference Power

• A Theory of Qualified Types
• Boxy Type-Inference for Higher-Rank Types and Impredicativity
• Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism
• Flexible Types: Robust Type Inference for First-class Polymorphism
• FPH: First-Class Polymorphism for Haskell
• MLF: Raising ML to the Power of System-F
• Practical Type Inference for Arbitrary-Rank Types
• QML: Explicit, First-Class Polymorphism for ML
• Wobbly Types: Type Inference for GADTs

Monadic Contexts

• Supermonads

Refinement Typing and Compiler Assistance

• Abstract Refinement Types
• Liquid Types
• Towards a Provably Correct Encoding from F* to SMT

Rows

• Abstracting Extensible Data Types
• Algebraic Subtyping
• Extensible Records with Scoped Labels

Types and Performance

• A Lazy Language Needs a Lazy Type System
• Higher-Order Type-Level Programming in Haskell
• Levity Polymorphism
• Partial Type-Constructors
• Theory and Practice of Demand Analysis in Haskell

Usability

• Explaining Type Errors