This is a (hopefully) simple implementation of Quantitative Type Theory/Graded Dependent Types, in TypeScript.

Try it out at https://atennapel.github.io/qtt-ts

References:

• "Syntax and Semantics of Quantitative Type Theory"
• "A graded dependent type system with a usage-aware semantics", I followed the rules from here
• See https://github.com/AndrasKovacs/elaboration-zoo for an explanation of how the typechecking algorithm works.
• I used some of the rules from https://github.com/BramvanVeenschoten1/qtt

Run CLI REPL:

yarn install
yarn start

Typecheck file:

yarn install
yarn start example.p

Notes:

• this currently implements the 0, 1- (affine), 1, 1+ (relevant), * (unrestricted) rig (the five-point linearity semiring), but the typechecker can handle any partially ordered semiring
• application does not have the usage annotation, these will be infered from the function type
• lambda with unannotated usage will be * by default unless checked against a function type, then it will use the usage from the type

Currently done:

• basic type theory with dependent functions and type-in-type
• checks from graded dependent types
• void, unit, sigma and sum types
• induction on the types
• fixpoint type
• a "world" token to play around with

Will not be implemented:

• implicit arguments/unification
• instance arguments
• consistent universe hierarchy
• inductive datatypes

The language:

u ::= elements of partially ordered semigroup

t ::=
  Type                -- universe
  x                   -- variable
  (u x : t) -> t      -- pi/function type
  \(u x : t). t       -- lambda
  t t                 -- application
  let u x : t = t; t  -- let

  Void                -- void/empty type
  indVoid P x         -- void induction

  ()                  -- unit type
  *                   -- unit value
  indUnit P x p       -- unit induction

  (u x : t) ** t      -- sigma/pair type
  (t, t : t)          -- pair
  indSigma u t t t    -- sigma induction

  t ++ t              -- sum type
  Left t t t          -- left injection
  Right t t t         -- right injection
  indSum u t t t t    -- sum induction

  Fix t               -- fixpoint of a functor
  Con t t             -- constructor of fixpoint
  indFix u t t t      -- fix induction

  World               -- the world
  WorldToken          -- token to represent the world
  updateWorld u t t   -- update the world
  helloWorld t        -- print hello world