ieeemma/dependent-types

Dependently typed programming language

Dependent Types

This repository contains a compiler for a dependently typed language. The language borrows concepts and syntax from Idris, and is implemented in Haskell.

Usage

The project depends on the following tools:

• GHC
• Cabal
• Racket

These can be installed through the above links or using a package manager. On Ubuntu, the command sudo apt install ghc cabal-install racket will install the necessary tools.

The project can be built with cabal build, and the compiler can be run with cabal run dependent-types -- <file>. Examples to run can be found in the examples/ directory. This produces a Racket file that can be run with racket <file>.rkt.

The test suite can be run with cabal test --test-show-details=always --test-option "--color=always".

Roadmap

• Parser
  • AST powered by recursion-schemes
  • Expressions
  • Top-level definitions
• Static analysis
  • Dependent typing
    • Evaluation
    • Normalization
    • Unification
    • Bidirectional checking
• Compiler
  • Scheme backend
• Language support
  • Prelude of useful types
  • Examples
  • Documentation
• Tooling
  • CLI
  • Pretty errors powered by diagnose