rachel/pi
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
A typechecker for intensional MLTT without elaboration.
32 Commits 1 Branch 0 Tags 912 KiB
Idris 99.4%
Makefile 0.6%
9275d39107
Go to file
depsterr 9275d39107 slight parser optimization
2022-08-01 18:26:13 +02:00
src slight parser optimization 2022-08-01 18:26:13 +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 readme 2022-07-28 15:46:00 +02:00

README.md

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

TODO

  • Universes (a la tarksi)

  • Elaboration

    • Implicit arguments
    • Universe family application
      • Syntax level russel universes
      • Universe of all other universes? (universe polymorphism)

  • Inductives

    • Indexed inductives

Things that could be fun to do sometime eventually

  • Pattern matching in elaborator

  • Write down the rules

  • Performence optimisation?

  • Compile to scheme

References

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