Skip to content

A type checker for FreshMLTT, a dependent type theory with abstractable names together with an equational characterisation of freshness.

Notifications You must be signed in to change notification settings

mjustus/freshtt

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

1 Commit
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

freshtt

A type checker for FreshMLTT, a dependent type theory with abstractable names together with an equational characterisation of freshness inspired by the corresponding notion in Nominal Sets.

Usage

freshtt FILE

Syntax

A file consists of a semicolon-separated list of definitions

DEF_1;
...  ;
DEF_n

where each definition DEFi consists of a name (that later definitions can refer to) a type and a body (of that type):

ID : TERM = TERM

There's no syntactic distinction between types and terms. Terms are formed as follows

  • local definitions

      let ID : TERM = TERM in TERM
    
  • cumulative hierarchy of universes

      U n
    

    where n is an integer

  • universe of name sorts

      N
    
  • simple and dependent function types

      TERM -> TERM
      (ID1, ..., IDn : TERM) -> TERM
    

    The arrow -> can be replaced by the unicode right arrow character, .

  • simple and dependent name abstraction types

      [ID1, ..., IDn : TERM] -> TERM
      [TERM] TERM
    
  • function abstraction (domain-free)

      \ID1 ... IDn. TERM
      λID1 ... IDn. TERM
    
  • name abstraction (domain-free)

      !ID1 ... IDn. TERM
      αID1 ... IDn. TERM
    
  • local name abstraction (domain-full)

      ?ID : TERM. TERM
      νID : TERM. TERM
    
  • function application

      TERM TERM
    
  • concretion

      TERM @ ID
    
  • name swapping

      swap ID ID in TERM
    
  • type annotation

      TERM :: TERM
    

Some syntactic sugar:

  • Telescopic type syntax: consecutive dependent function and name abstractions can be written without a separating arrow (->), i.e. instead of

      (ID : TERM) -> [ID : TERM] -> ...
    

    we can write

      (ID : TERM) [ID : TERM] -> ...
    

Hacking

  • parser.mly: parser for freshtt programs
  • raw.ml: abstract syntax close to concrete syntax and a pretty-printer
  • term.ml: internal syntax (note that Fun and Nab are non-binding!)
  • eval.ml and readback.ml: NbE-style normalisation procedure. In particular, eval performs weak-head normalisation and rb_nf eta expands and reduction under alpha- and lambda-abstractions.
  • model.ml: values in the NbE model. Alpha- and lambda-abstractions are represented by Term.t closures.
  • normal.ml: normal forms
  • check.ml: bidirectional type checker

References

  1. A. Abel, Normalization by Evaluation: Dependent Types and Impredicativity.
  2. T. Coquand, An algorithm for type-checking dependent types.
  3. M. J. Gabbay, A. M. Pitts, A New Approach to Abstract Syntax with Variable Binding.
  4. A. M. Pitts, J. Matthiesen and J. Derikx, A Dependent Type Theory with Abstractable Names.

About

A type checker for FreshMLTT, a dependent type theory with abstractable names together with an equational characterisation of freshness.

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published