Pledge

Pledge is a small language for learning restricted dependent types. This page is an editor that checks a Pledge program as you type and shows what the type checker knows at the caret. It needs JavaScript to run the checker.

Other pages: the tutorial, the specification, the example programs and the repository.

The program the editor starts with:

data Nat() : Type() {
  Zero() : Nat();
  Succ(pred : Nat()) : Nat();
}

data Vec(A : Type(), n : Nat()) : Type() {
  VNil(A : Type()) : Vec(A, Zero());
  VCons(A : Type(), n : Nat(), head : A, rest : Vec(A, n))
    : Vec(A, Succ(n));
}

fn vhead(A : Type(), n : Nat(), v : Vec(A, Succ(n)))
    -> (x : A) {
  let VCons(_, _, hd, _) = v;
  hd
}

let x = VCons(Nat(), Zero(), Zero(), VNil(Nat()));
print vhead(Nat(), Zero(), x);