A Super Kawaii Dependently Typed Programming Language
The developer of this repository has not created any items for sale yet. Need a bug fixed? Help with integration? A different license? Create a request here:
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 exec -- dtt -t PATH/TO/Foo.dtt.
$HOME/.local/binis in your
stack installin this directory.
dtt -t PATH/TO/Foo.dttto type check a file.