#+title: 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.

(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))) #+end_src

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

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

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

Bramble

Install / Use