Skip to content

Latest commit

 

History

History
40 lines (27 loc) · 1.55 KB

README.md

File metadata and controls

40 lines (27 loc) · 1.55 KB
Raw

System-F with bidirectional type inference

This project implements System-F with bidirectional type inference and type application synthesis as described in Pierce and Turner's Local Type Inference. Our system can handle the following cases:

  • omit type annotations on lambda functions when they are at the argument position in some function application
  • when applying a function of type (all (a) (t1 -> t2)), we will try to infer the type of arguments, then use the type of arguments to determine what a should be instantiated to and insert the corresponding type application
  • when checking a lambda term against a universal type, we automatically insert type abstraction

Syntax

  • (Lam (x1 x2 ... xn) e) means Λx1x2…xn.e,
  • (@ e t1 t2 ... tn) means e[t1][t2]…[tn] and
  • (all (a1 a2 ... an) t) means ∀a1a2…an.t.

Tests

These features are demonstrated in the following tests:

  • tests/forall_annotated.stlc: basics of System-F
  • tests/forall_bidir.stlc: shows that we can omit type annotations on lambda functions
  • tests/application.stlc: shows that we can omit type applications when they can be inferred
  • tests/forall_nested.stlc: shows that we correctly implement types using De Bruijn indices

Testing in REPL

Use the following directives in coretop to load all required modules.

$ coretop
#mod_use "var.ml";;
#mod_use "testing.ml";;
#mod_use "env.ml";;
#mod_use "syntax.ml";;
#use "check.ml";;