Quick start

For readers already comfortable with dependent types. Skim the cheatsheet, run a program, then dive into the reference.

1. Install

One line on Linux (x86_64 or aarch64) and macOS (Apple Silicon):

curl -fsSL https://violet-lang.org/install.sh | sh

The script downloads the latest release binary into ~/.violet/bin/, verifies its SHA-256 checksum, and appends a PATH line to your shell's rc file.

Pin a specific version:

VIOLET_VERSION=v0.6.1 sh -c "$(curl -fsSL https://violet-lang.org/install.sh)"

Skip the PATH edit, or change the install prefix:

VIOLET_NO_MODIFY_PATH=1 sh -c "$(curl -fsSL https://violet-lang.org/install.sh)"
VIOLET_PREFIX=/opt/violet  sh -c "$(curl -fsSL https://violet-lang.org/install.sh)"

To uninstall, remove ~/.violet/ and delete the # >>> violet path >>> block from your shell's rc file.

2. Start a project

Scaffold a new project:

violet new hello

This creates a hello/ directory with an info.vt manifest:

\name "hello"
\version "0.1.0"

Other useful commands: violet add KEY URL declares a git dependency, violet update resolves dependencies into info.lock, and violet check type-checks your code.

3. A first program

Put this in hello/main.vt:

\universe 𝓤

\data Nat : 𝓤
  | zero : Nat
  | suc : Nat -> Nat

\let add : (m n : Nat) -> Nat \where
  add m n <= \elim m
  | add zero n => n
  | add (suc m) n => suc (add m n)

\operator "\x + \y" => add x y
  \associativity: \left

Type-check it:

cd hello
violet check main.vt

4. Cheatsheet

# inductive type
\data T [params] : [indices ->] 𝓤
  | ctor1 : ...
  | ...
  | ctorn : ...

# function with clauses
\let f args : T \where
  f args <= \elim x
  | ...

# record (with eta)
\record R : 𝓤
  | field : T

# user-defined operator
\operator "\x ⊕ \y" => f x y
  \associativity: \left
  \stronger_than: +

# module boundaries (private by default)
\import nat
\export Nat add

Each construct above has its own page under Reference.