No results found

violet

A programming language, half theorem prover

violet

builds.sr.ht status

Warning The project still in early stage.

A programming language focuses on

  • dependent type
  • effect system
  • semantic versioning
  • separate compilation

Usage

Load module into REPL

violet example/module.vt
Example
data Unit | unit

data Nat
  | zero
  | suc Nat

data Bool
  | true
  | false

def zero? (n : Nat) : Bool =>
  match n
  | zero => true
  | suc _ => false

record T
  | a : Nat
  | b : Bool

def t (x : Nat) : T => (x, zero? x)

Develop

You will need to install lean, via any package manager would be fine. Especially recommend vscode plugin (https://marketplace.visualstudio.com/items?itemName=leanprover.lean4), install it and wait, it should install elan, lean, and lake for you.

Build the project

lake build
Theory

Here are some related theories we already applied or going to use.

  • elaboration1
  • universe polymorphism2 will try mugen
  • termination checker3 will use lexicographic recursion
  • type class4
  • indexed data type5

Footnotes

  1. Elaboration with first-class implicit function types: https://dl.acm.org/doi/10.1145/3408983 ↩

  2. An Order-Theoretic Analysis of Universe Polymorphism: https://favonia.org/files/mugen.pdf ↩

  3. foetus - Termination Checker for Simple Functional Programs: https://www2.tcs.ifi.lmu.de/~abel/foetus.pdf ↩

  4. Tabled Typeclass Resolution: https://arxiv.org/pdf/2001.04301.pdf ↩

  5. A SIMPLER ENCODING OF INDEXED TYPES: https://arxiv.org/pdf/2103.15408v4.pdf ↩