Skip to content
<open-source>
Oeiuwq Faith Blog OpenSource Porfolio

ditto/ditto

A Super Kawaii Dependently Typed Programming Language
Source code at GitHub https://github.com/ditto/ditto
ditto/ditto.json
{
  "createdAt": "2015-08-02T05:11:35Z",
  "defaultBranch": "master",
  "description": "A Super Kawaii Dependently Typed Programming Language",
  "fullName": "ditto/ditto",
  "homepage": "",
  "language": "Haskell",
  "name": "ditto",
  "pushedAt": "2018-07-12T13:00:17Z",
  "stargazersCount": 176,
  "topics": [
    "dependent-types",
    "programming-language",
    "proof-assistant",
    "type-theory"
  ],
  "updatedAt": "2025-10-04T20:21:28Z",
  "url": "https://github.com/ditto/ditto"
}

Ditto

Section titled “Ditto”

Build Status

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.

Ditto

Features

Section titled “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

Section titled “Missing Features”
  • Universe hierarchy (currently Type : Type)
  • Termination checker
  • Positivity checker

Development

Section titled “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

Section titled “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.