Dependently typed programming language written in Haskell. Code is based on https://github.com/AndrasKovacs/elaboration-zoo and https://gist.github.com/AndrasKovacs/d5d78d8e556d91afb1f724d1c2246b6b.
Start REPL
stack run repl
Elaborate an expression
stack run < expr.txt
Elaborate definitions
stack run elab-defs < defs.txt
Currently supports:
- pi-types
- sigma-types
- Void, Unit, Bool primitive types
- heterogenous equality type with axiom K
- predicative non-cumulative hierarchy of universes, with simple universe polymorphism
- "Gentle art of Levitation"-style descriptions
- simple instance arguments (
{{_ : Functor F}} -> ...)
TODO:
- core language
- syntax
- levels
- values
- verification
- surface language
- syntax
- parser
- elaboration
- primitives
- holes
- globals
- definitions
- modules
- metas
- unification
- zonking
- update elaboration
- named holes
- implicit functions
- level metas
- basic level metas
- levels in pi/sigma
- update elaboration
- lam and app with level renaming
- descriptions
- Desc and Data constructors
- Ex and El
- bidirectional Con
- levitation
- conversion of indBool and ifDesc
- Data elimination
- simplify equality type
- Refl as a core term
- rename HEq to Id
- instance search
- basic instance search
- postpone and retry
- instance parameters
- limit instance search
- instance definitions
- instance lets
- recursive instance search
- naming fixes
- give fresh names to _ names if used
- generate nicer fresh names
- erased parameters
- lib updates
- induction for SumD and SumDL
- induction deriviation
- update unification
- eta rule for Bool
- more cumulativity in elaboration
- improve level unification
- pruning
- postponing
- improved unfolding
- selective unfolding in holes
- unfolding annotations on definitions
- unfold if progress is made
- add more syntax
-
\.for lambdas with no parameters (like Haskell's$) - infix operators
- nat literals
- defs and lets with parameters
- list and vector literals
-
- improve error message
- use source position
- more types
- nested fixpoints
- coinductive types
- mixed fixpoints
- nested types
- inductive-recursive types
- inductive-inductive types
- curried indexes and parameters
- Prop universe
- Setoid type theory/observational type theory
Level solver issues:
- max '4 ?l7 ~ S '4
- max (S ?l0) ?l1 ~ max (S '3) '2