A Super Kawaii Dependently Typed Programming Language
Ditto is a super kawaii dependently typed programming language. It is super kawaii due to its small and straightfoward implementation, and adorable syntax ;)
Taking advantage of its simple implementation, we use Ditto as a vehicle for experimenting with type system features. Despite being implemented simply, Ditto is a high-level language that supports terse programs, rather a core language necessitating verbose encodings.
Put together, these things make Ditto a good language for research. When confronted with a simple versus performant implementation decision, we tend to choose the former. For now, we are concerned with type checking code rather than running code.
stack build
.stack test
.stack ghci
.stack exec -- dtt -t PATH/TO/Foo.dtt
.$HOME/.local/bin
is in your $PATH
.stack install
in this directory.dtt -t PATH/TO/Foo.dtt
to type check a file.