About Violet

Violet is a small, experimental dependently typed language.

Language features

Top level

• \let for definitions
• \import for bringing in modules
• \data for inductive types — with auto-generated eliminators like Nat-elim and a strict-positivity check
• \export name+ — top-level definitions are private by default

Terms

• variables, applications
• typed lambdas and plain lambdas
• universes (with universe polymorphism)
• holes for incremental development
• builtin record types with eta

Pattern matching

Violet uses a small stack-based syntax to drive elaboration:

• <= \elim splits on a scrutinee,
• <= \intro introduces an variable, and
• <= \split opens up a record.

Clauses are written one at a time, which keeps the surface syntax close to the elaborator’s actual moves.

Status

Violet is in active development. Expect rough edges, missing documentation, and breaking changes. Feedback and experiments are very welcome.