Gradual type systems

Type systems are useful because they allow for added precision in programs. They ensure that programs satisfy the properties specified in the type declarations, thereby reducing bugs. The effort required to come up with type declarations (i.e. thinking about the properties of functions, their arguments, and their return values) is necessary anyway, and type annotations allow us to formalise this.

However, migrating codebases from one type system (or no type system) to another can be incredibly difficult with traditional type systems. Because these systems forbid type mismatches, new type annotations must be added all at once.

Gradual type systems solve this problem by allowing type annotations to be added incrementally. Essentially, they allow us to model uncertainty — when we don't know what the new type annotation is, we can just leave it unknown.

Gradual type systems are commonly intended to migrate dynamically typed programs to ordinary statically typed programs, but they can also be developed to cover migration between any two type systems, such as between static and refinement type systems. (Refinement types are like static types enriched with predicates. If you've heard of liquid types, those are a form of refinement types!) Fundamentally, these systems support migration between systems that are "more" or "less" static than one another.

Enter the diamond

The outcome of this project is a gradual type system with a unifying connective that allows the expression of all possible varieties of gradual types instead of being defined with two specific "endpoint" type systems. This connective, the "diamond type", also isolates uncertainty in a single binary connective ♢ while maintaining typing guarantees.

The annotation A ♢ B describes a value that has either type A or B (A ⋁ B), but is treated by the type system as having both type A and B (A ⋀ B). Because ♢ is introduced like ⋁ and eliminated like ⋀, it allows the specification of "at least one of" relationships.

This provides a greater level of control over type specifications. If a programmer knows that something has one of type {A, B, C}, they can use the annotation A ♢ B ♢ C during the process of figuring out what the actual type is, instead of having to leave it unknown like in traditional gradual type systems.

When you're solving a Sudoku puzzle, it's helpful to list possible values for each square in the corners and eliminate them until you know which one must be the actual square value. This type system lets you do just that for type annotations! It can also be useful for functions that work equivalently on arguments of different types, for example in languages with multiple integer types like Go.

Normally, the "gradual parts" of a gradual type system need to be implemented from first principles separately. In this project, all these "gradual parts" are built on top of one unifying connective (the diamond), which is the foundation of all "gradualness" or uncertainty. This gives greater mathematical elegance. As well, it will hopefully be easier to prove things about the language because there won't be as much "stuff" in it.

Implementation

Implementing this type system involves a type checker (for the type system) and an interpreter (for the operational semantics). This begins with the implementation of the simply typed lambda calculus and sum types, and ends with target program generation.

Haskell — a strongly-typed, lazily-evaluated, and purely functional programming language — was chosen to implement this project.

module Main where

type Name = String

data Expr
  -- standard expressions
  = EVar Name       -- name of each variable
  | EAbs Name Expr  -- lambda abstractions
  | EApp Expr Expr  -- lambda applications
  | EAnno Expr Type -- type annotations
  | EInj1 Expr      -- injections
  | EInj2 Expr      -- injections
  | ECase Expr (Name, Expr) (Name, Expr) -- cases
  -- literals
  | EUnit
  | EInt Int
  -- binary operations
  | EAdd Expr Expr
  | ESub Expr Expr
  | EMlt Expr Expr
  | EDiv Expr Expr
  -- diamonds
  | EDia Expr Name Expr
  deriving (Show)

data Type
  = TUnit
  | TInt
  | TArr Type Type  -- functions
  | TSum Type Type  -- sums
  | TDia Type Type  -- diamonds
  deriving (Show, Eq)

data EnvElem = EnvElem Name Type
type Env = [EnvElem]

coerce :: Type -> Type -> Bool
coerce tA tB = (tA == tB)

lookupVar :: Env -> Name -> Maybe Type
lookupVar [] _ = Nothing
lookupVar ((EnvElem x' t'):rest) x
  | x == x' = Just t'
  | otherwise = lookupVar rest x

check :: Env -> Expr -> Type -> Bool
-- ChkUnitIntro
check env EUnit TUnit = True
-- ChkIntIntro
check env (EInt _) TInt = True
-- ChkArrowIntro
check env (EAbs x e0) (TArr tA tB) =
  check ((EnvElem x tA):env) e0 tB
-- ChkSumIntro
check env (EInj1 e0) (TSum tA1 tA2) =
  check env e0 tA1
check env (EInj2 e0) (TSum tA1 tA2) =
  check env e0 tA2
-- ChkSumElim
check env (ECase e0 (x1, e1) (x2, e2)) tB =
  case synth env e0 of
    Just (TSum tA1 tA2) ->
      check ((EnvElem x1 tA1):env) e1 tB &&
      check ((EnvElem x2 tA2):env) e2 tB
    _ -> False
-- ChkDiaIntro
check env e (TDia tA1 tA2) =
  check env e tA1 || check env e tA2
-- ChkDiaElim
check env (EDia e0 x e) tB =
  case synth env e0 of
    Just (TDia tA1 tA2) ->
      check ((EnvElem x tA1):env) e tB ||
      check ((EnvElem x tA2):env) e tB
    _ -> False
-- ChkCSub
check env e tB =
  case synth env e of
    Just tA -> coerce tA tB
    _ -> False

synth :: Env -> Expr -> Maybe Type
-- SynVar
synth env (EVar x) = lookupVar env x
-- SynAnno
synth env (EAnno e0 tA) =
  if check env e0 tA
  then Just tA
  else Nothing
-- SynArrowElim
synth env (EApp e1 e2) =
  case synth env e1 of
    Just (TArr tA tB) ->
      if check env e2 tA
      then Just tB
      else Nothing
    _ -> Nothing
-- SynDiaElim
synth env (EDia e0 x e) =
  case synth env e0 of
    Just (TDia tA1 tA2) ->
      case synth ((EnvElem x tA1):env) e of
        Just tB1 -> case synth ((EnvElem x tA2):env) e of
          Just tB2 -> Just (TDia tB1 tB2)
          Nothing -> Just tB1
        Nothing -> synth ((EnvElem x tA2):env) e
    _ -> Nothing

main :: IO ()
main = undefined

Limitations and future work

  • Coercion: Currently, the coerce function only checks for simple type equality. A complete implementation would also need to determine when one type can safely satisfy another.
  • Evaluation contexts: Full synthesis and checking for diamonds requires evaluation contexts to step through expressions and try to "find" the diamonds. This requires a lot of substitution and back-tracking. Instead, this project introduces a "diamond expression" that represents expressions with diamond types, so that they don't have to be sought out. This simplifies the implementation at the cost of extra work for the programmer.
  • Target program generation: The type checker does not yet generate target terms. Supporting this will require modifications to check and synth.
  • Assessment: The type checker needs more testing, both to ensure correct functionality and to determine the feasibility of the operational semantics.
  • Parser: A parser for a language using this type system is in the early stages of development.

Acknowledgements

I'm grateful to Prof. Jana Dunfield, who developed the diamond type mechanism that I implemented in this project. Her guidance (and banter) was especially appreciated while I was silly enough to take on multiple thesis courses at once.