ditto / Ditto
Licence: gpl-3.0
A Super Kawaii Dependently Typed Programming Language
Stars: ✭ 154
Programming Languages
haskell
3896 projects
Labels
Projects that are alternatives of or similar to Ditto
lplzoo
Fine-grain implementations of common lambda calculi in Haskell, tested with QuickCheck
Stars: ✭ 32 (-79.22%)
Mutual labels: type-theory
Datafun
Research on integrating datalog & lambda calculus via monotonicity types
Stars: ✭ 287 (+86.36%)
Mutual labels: type-theory
Pikelet
A friendly little systems language with first-class types. Very WIP! 🚧 🚧 🚧
Stars: ✭ 485 (+214.94%)
Mutual labels: type-theory
Rust Nbe For Mltt
Normalization by evaluation for Martin-Löf Type Theory with dependent records
Stars: ✭ 72 (-53.25%)
Mutual labels: type-theory
Type-Theory
Lecture note on Lambda Calculus and Types for FLOLAC
Stars: ✭ 26 (-83.12%)
Mutual labels: type-theory
Foundational Knowledge For Programmers
List of resources about foundational knowledge for programmers (supposed to last a few decades)
Stars: ✭ 115 (-25.32%)
Mutual labels: type-theory
Typedefs
Programming language agnostic type construction language based on polynomials.
Stars: ✭ 337 (+118.83%)
Mutual labels: type-theory
Write You A Haskell
Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)
Stars: ✭ 3,064 (+1889.61%)
Mutual labels: type-theory
Agda
Agda is a dependently typed programming language / interactive theorem prover.
Stars: ✭ 1,699 (+1003.25%)
Mutual labels: type-theory
types-and-programming-languages
Exercises from Benjamin Pierce's "Types and Programming Languages" textbook + extras!
Stars: ✭ 92 (-40.26%)
Mutual labels: type-theory
Narc Rs
(WIP) Dependently-typed programming language with Agda style dependent pattern matching
Stars: ✭ 58 (-62.34%)
Mutual labels: type-theory
Formal Type Theory
Formalising Type Theory in a modular way for translations between type theories
Stars: ✭ 74 (-51.95%)
Mutual labels: type-theory
Ditto
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.
Features
- Open universe of types.
- Dependent pattern matching.
- Searches all possible coverings.
- Enhanced catch-all clauses (novel).
- Implicit arguments.
- Miller-pattern unification.
- Constraint postponement.
- Mutual definitions.
- Functions.
- Induction-recursion.
- Induction-induction.
- Eta-equality for functions.
- Interactivity via command-line interface.
- Holes.
- Case splitting.
- Tracking user vs machine-introduced variables.
Missing Features
- Universe hierarchy (currently Type : Type)
- Termination checker
- Positivity checker
Development
- Make sure you have Stack installed.
- Build the project with
stack build
. - Run the tests with
stack test
. - Work interactively with
stack ghci
. - Run the current version of the binary with
stack exec -- dtt -t PATH/TO/Foo.dtt
.
Installation
- Make sure you have Stack installed.
- Make sure
$HOME/.local/bin
is in your$PATH
. - Run
stack install
in this directory. - Run
dtt -t PATH/TO/Foo.dtt
to type check a file.
Note that the project description data, including the texts, logos, images, and/or trademarks,
for each open source project belongs to its rightful owner.
If you wish to add or remove any projects, please contact us at [email protected].