Skip to content
/ algaett Public

๐Ÿฆ  An experimental elaborator for dependent type theory using effects and handlers

License

Notifications You must be signed in to change notification settings

RedPRL/algaett

Folders and files

NameName
Last commit message
Last commit date

Latest commit

ย 

History

85 Commits
ย 
ย 
ย 
ย 
ย 
ย 
ย 
ย 
ย 
ย 
ย 
ย 
ย 
ย 
ย 
ย 
ย 
ย 
ย 
ย 
ย 
ย 

Repository files navigation

๐Ÿฆ  algaettโ€™s not algaeff

This development is an experiment with the following goals:

  1. Adopt smalltt and related techniques into the cubical world.
  2. Show how various OCaml packages of ours fit together.
  3. Write natural grammars without neccesarily conforming to LR(k).
  4. Use lots of Unicode emojis.

Try It Out!

opam pin git+https://github.com/RedPRL/bantorra
opam pin git+https://github.com/RedPRL/algaett
cat tests/example.ag
algaett tests/example.ag

The last line should not have an output, which means it type checks!

Important Ideas

Ideas from Smalltt

The core NbE algorithm closely follows Andrรกs Kovรกcsโ€™s smalltt. Here are some notable differences:

  1. We intentionally do not implement unification.
  2. The universe itself (as a term) is not inferable, which means that the checking might have to be redone with the type unfolded.
    ๐Ÿ“Œ ๐Ÿ˜„ : ๐ŸŒŒ ๐Ÿ†™ 2๏ธโƒฃ ๐Ÿ‘‰ ๐ŸŒŒ ๐Ÿ†™ 1๏ธโƒฃ
    ๐Ÿ“Œ _ ๐Ÿ‘‰ ๐ŸŒŒ : ๐Ÿ˜„
    
    The type inference from the universe ๐ŸŒŒ will fail, and then the type checking will be redone with ๐Ÿ˜„ unfolded to ๐ŸŒŒ ๐Ÿ†™ 1๏ธโƒฃ.
  3. The conversion checker is generalized to handle subtyping generated by cumulativity.

Modular Development

  • algaeff: reusable effects-based components
  • asai: error messages (not actively used yet)
  • bantorra: unit resolution (not actively used yet)
  • bwd: backward lists
  • mugen: universe levels
  • yuujinchou: namespaces and name modifier

Parser beyond LR

We are using the Earleyโ€™s parsing algorithm which can handle all context-free grammars.

Documentation

Here is the API documentation.

Releases

No releases published

Contributors 4

  •  
  •  
  •  
  •  

Languages