startling / coatl

silly dependently-typed language

coatl

coatl is a work-in-progress dependently typed type-checker and evaluator. One day it will grow up to be a compiler.

The only target executable here is coatli, an interactive interpreter. It's usable now! There are three built-ins -- Type, the type of Types, (->), a constructor of function types, and (~), which is used to represent the dependent function space.

We can use (~) to represent the easily:

the : Type ~ { a => a -> a };
the _ a = a;

Functions with multiple dependent parameters, though, become unwieldy:

const : Type ~ { a => Type ~ { b => a -> b -> a } };
const _ _ a _ = a;

An improvement to this situation is planned.

Reading List

• A Tutorial Implementation of a Dependently-Typed Calculus by Andres Löh, Conor McBride and Wouter Swierstra
• Eliminating Dependent Pattern-Matching, by Healfdene Goguen, Conor McBride, and James McKinna
• Idris, a General Purpose Dependently-Typed Programming Language: Design and Implementation, by the esteemed Edwin Brady.
• Towards a practical programming language based on dependent type theory, by Ulf Norell

coatl's Issues

Environments.

We don't have anything nice going on with environments -- there are no modules, no packages, no imports. This is partially by design, but it would be nice if we could abstract e.g. L.C.Check, L.C.C.Types, L.C.Evaluate et al. for arbitrary environmenty things.

After this we can do nice things like load and unload modules freely in coatli.

Preserve original source and type.

When you annotate something with a type, you want e.g. :t in coatli to tell you the type you annotated it with.

A :s[ource] command might be useful, too.

This is probably intertwined with #1, in that a more general notion of an environment might have provisions for finding source information.

`L.C.C.Types` is terrible.

Look at it. What in the world is a Checking? There's a Prism' in it??. Ideally a future implementation would avoid that stupid trick and not be founded in explicit recursion, especially since we have so many nice interfaces to Terms -- Traversable, Monad, Applicative, etc etc.

There are tests, and the code (as of commit 01f2051) is decoupled nicely from L.C.Check, so this will probably be relatively straightforward.

This is intertwined in a complicated way with #1 -- not sure which should go first.

New pretty-printer.

ansi-wl-pprint isn't so great for a number of reasons:

• It dictates that style and content be intertwined
• It doesn't let use do fancier things with style, like indenting each indented line of some output.
• Its hinting for indentations and linebreaks could be expanded.

In addition, a number of the combinators are sort of useless for our purposes.