A typechecker for intensional MLTT without elaboration.
Go to file
2022-08-22 20:49:49 +02:00
src align arrows 2022-08-06 02:32:09 +02:00
tests update readme 2022-07-28 15:46:00 +02:00
.gitignore initial commit 2022-04-23 15:18:06 +02:00
makefile definition system, repl 2022-07-26 23:07:13 +02:00
pi.ipkg definition system, repl 2022-07-26 23:07:13 +02:00
README.md update expectations in readme 2022-08-22 20:49:49 +02:00

pi

A dependently typed system

Implemented

  • A Basic dependent lambda calculus

    • lambda abstractions
    • variables
    • pi types
    • type of types
  • let … in …

  • Unit type

  • Empty type

  • Natural numbers

  • Σ Types

  • Martin-Löf Identity types

Lacking

Here are some things which are not present but could be.

This project has served me well by teaching me about typechecking dependently typed systems. Its likely that the features listed below will not be implemented as Ill move onto other projects and learn more about elaboration.

  • Universes
    • a la tarksi
  • Inductives
    • W types
    • Indexed inductives
  • Elaboration
    • Implicit arguments
    • Universe family application
      • Syntax level russel universes
      • Universe of all other universes? (universe polymorphism)

References

Some of the material I found helpful in groking dependent type checking: