Bramble

Bramble is a dependently-typed programming language, written using S-expressions. As in Coq, there are really a few distinct “languages” involved:

• The expression language (or calculus), which is a dependently-typed lambda calculus supplemented with (parametric, recursive) algebraic datatypes, records, and fixpoint.
• The vernacular, which tells the system what expressions to evaluate, typecheck, and compile.

In practice, this ends up working in exactly the way you’d expect from any other ML/Haskell-like functional language.

An example

(data Nat () Z (S Nat))

(check Nat Type)
(check Z Nat)

(define add (∀ ((_ : Nat) (_ : Nat)) Nat)
  (λ (x y)
    (case x
      (Z y)
      (S (λ (n) (S (add n y)))))))

(infer (add (S Z) (S Z)))
(debug (add (S Z) (S Z)))

Goals

• A language with a powerful type system that is trivial to extend with new compilation targets
• Those compilation targets can be weird, not just “mainstream” languages (DSLs for other programs, scripts inside game engines, etc.)
• Adding new targets should be a “normal” workflow that doesn’t require deep knowledge of compiler internals
• Explicit is better than implicit, always: hide resulting verbosity with macros if necessary
• Completely uniform syntax (Coq is pretty good at this, Haskell is not :[)
• It’s worth sacrificing speed for versatility (e.g. in compilation targets), always
• Trusting proofs in an unsound system requires a better “cheating heuristic” than just searching for “Admitted.”, but it’s still possible

Features

• Recursive/parametric algebraic datatypes (not GADTs yet, since there are only parameters, not indices)
• Record subtyping
• Unrestricted fixpoint. This is a design choice that leads to:
• Type : Type, because who cares about Girard’s paradox when ∀(a : Type). a is already inhabited

Non-features

• Type inference
• Any kind of inference of anything, really, including implicit arguments and “typeclass instances” (records)

Future plans (decreasing priority)

• More vernacular directives, evaluate/typecheck from CLI rather than from REPL
• Typesafe macros
• Compiler backends as data
• Better error messages/backtraces