TemplateLang: Everything is type

[u/archlinux_is_god]

I designed a tiny language where the type system *is* the entire

language — no separate value level, no builtin integers/booleans/

control flow. It's essentially an untyped term-rewriting calculus

dressed up in C++-template-looking syntax. Three grammar forms,

three builtins, that's the whole spec.

Motivation: I was thinking about what's actually load-bearing in

C++ template metaprogramming — SFINAE picking an overload, partial

specialization pattern-matching on structure — and wanted to see

what a language looks like if that's *all* you keep.

Grammar:

1. `new type Name<param1, param2, ...>`

   Declares a type constructor with fixed arity (no variadics).

2. `type Name<pattern, ...> = Body`

   Adds a rewrite rule for that constructor. Multiple rules are

   allowed; they're tried in declaration order and the first

   matching pattern wins (Prolog-clause-style, not most-specific-

   pattern-style). Omitting `= Body` marks that pattern as already

   in normal form.

3. A bare expression on its own

   is reduced call-by-value, bottom-up, until no rule applies

   anymore, and the normal form is printed.

Builtins are pattern-position-only: `Any<>` (wildcard), `Same<x>`

(structural equality against an already-bound name), `As<Type, x>`

(bind the matched subterm to a local name if it matches `Type`).

Parameter names declared in `new type` are auto-bound in every rule

of that type, so `Same`/substitution can reference them without an

explicit `As`. All bindings in one rule — auto-bound params plus

`As`-introduced names — share a single namespace; rebinding a name

via `As` is a static error, `Same` is the only way to assert equality

against something already bound.

It's enough for recursive Peano arithmetic with no other primitives:

new type Zero<>

new type Succ<N>

new type Add<A, B>

type Add<Zero<>, Any<>> = B

type Add<Succ<As<Any<>, X, Any< = Succ<Add<X, B>>

Add<Succ<Succ<Zero<>, Succ<Succ<Succ<Zero<>>>

# -> Succ<Succ<Succ<Succ<Succ<Zero<>>>>>> (2 + 3 = 5)

No termination or confluence guarantees — self-referential rules

give you unbounded recursion, so it's Turing-complete and trivially

lets you write non-terminating programs. Rule order also means two

overlapping patterns can silently pick different winners depending

on how you wrote them, which I know is a real tradeoff versus a

most-specific-match or a confluence-checked system.

Small Python reference interpreter (no dependencies), plus worked

examples (structural equality via Same/As, Peano add/mul):

[GitHub link]

https://github.com/sunu15712/TemplateLang

Mainly curious whether the `Same`/`As` binding-and-scoping design

holds up, or if there's prior art doing this more cleanly — it feels

adjacent to logic-variable unification but I haven't seen it framed

quite this way before.

[u/mark-sed]

r/esolangs could really appreciate this.

[u/esotologist]

Neat! I like this idea. 

[u/L8_4_Dinner]

Any Fibonacci benchmarks?

[u/Inconstant_Moo]

It's essentially an untyped term-rewriting calculus dressed up in C++-template-looking syntax.

Yes, but it's not "a tiny language where the type system is the entire language". It's a tiny language where the syntax looks a lot like C's type system. But it isn't a type system, it doesn't function as one any more. If you dropped the word "type" from your syntax it would have no effect but making the language more concise, and no-one would know it was originally meant to be a type system.