ditto

by ditto

ditto /ditto

A Super Kawaii Dependently Typed Programming Language

148 Stars 5 Forks Last release: Not found GNU General Public License v3.0 348 Commits 0 Releases

Available items

No Items, yet!

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

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

  • 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.

We use cookies. If you continue to browse the site, you agree to the use of cookies. For more information on our use of cookies please see our Privacy Policy.