Calculus of Constructions
A lightweight implementation of the Calculus of Constructions in JavaScript. CoC is both a minimalistic programming language (similar to the Lambda Calculus, but with a very powerful type system) and a constructive foundation for mathematics, serving as the basis of proof assistants such as Coq.
Features
-
Core lang with
Lambda
,Forall
,Application
,Variables
and, as you love paradoxes,Fix
andType in Type
. -
Let
bindings as syntax sugars. -
Extremelly minimalistic, unbloated, pure ASCII syntax.
-
Completely implemented with HOAS, substitution free, including the type checker, which means it is very fast.
-
A robust parser, which allows arbitrary grammar nestings, including of
Let
s. -
A smart stringifier which names vars so that combinators are stringified uniquely, regardless of the context.
-
Node.js, cross-browser, 100% ES5 compliant.
-
Simple command line interface to type-check / evaluate a file.
-
Can deal with files, solve devs recursively, auto-imports missing names.
-
Can pretty-print terms showing names for known combinators.
-
All that in less than 400 lines of code, ang a gziped minified size of just
2.3kb
.
Usage
Install:
$ npm install -g calculus-of-constructions
From command line:
The command line can be used to print the base form, the normal form, and the type of a term. It auto-includes undefined variables by detecting them on the same directory. It can either print the full form, or a short form with known names.
$ coc two # (a:* (b:(.a a) (a:a (b (b a))))) $ coc type "(exp two two)" # Nat $ coc norm "(exp two two)" # four $ coc full "(exp two two)" # ((c:(a.* (.(.a a) (.a a))) (b:(a.* (.(.a a) (.a a))) (a:* (b (.a a) (c a))))) (a:* (b:(.a a) (a:a (b (b a))))) (a:* (b:(.a a) (a:a (b (b a)))))) $ coc full type "(exp two two)" # (a.* (.(.a a) (.a a))) $ coc full norm "(exp two two)" # (a:* (b:(.a a) (a:a (b (b (b (b a)))))))
Check out the examples for that usage.
From JavaScript:
const coc = ; const main = `T:* x:T x`; // id function const term = CoC; // parses source, could be an object {name: source, ...}const type = CoCtypeterm; // infers typeconst norm = CoC; // normalizes console; // prints original termconsole; // prints inferred typeconsole; // prints normal form // CoC.show can receive, optionally, a function that// receives a combinator and returns a name of it.
Syntax
-
Lambda:
name:Type Body
A function that receives
name
of typeType
and returnsBody
. -
Forall:
name.ArgType BodyType
The type of functions that receive
name
of typeArgType
and returnBodyType
. -
Fix:
self@ Term
The term
Term
with all instances ofself
replaced by itself. -
Apply:
(f x y z)
The application of the function
f
tox
,y
andz
. -
Let:
name=Term Body
Let
name
be the termTerm
inside the termBody
.
The name can be omitted from Lambda
and Forall
, so, for example, the equivalent of Int -> Int
is just .Int Int
. All other special characters are ignored, so you could write λ a: Type -> Body
if that is more pleasing to you.
Example:
Below, an example implementation of exponentiation:
Nat= Nat. * Succ. (.Nat Nat) Zero. Nat Nat two= Nat: * Succ: (.Nat Nat) Zero: Nat (Succ (Succ Zero)) exp= a: Nat b: Nat Nat: * (b (.Nat Nat) (a Nat)) (exp two two)
You can save it as exp.coc
and run with coc eval exp.coc
.
To aid you grasp the minimalist syntax, it is equivalent to this Idris program:
NatT : TypeNatT = (Nat : Type) -> (Succ : Nat -> Nat) -> (Zero : Nat) -> Nat two : NatTtwo = \ Nat : Type => \ Succ : (Nat -> Nat) => \ Zero : Nat => Succ (Succ Zero) exp : NatT -> NatT -> NatTexp = \ a : NatT => \ b : NatT => \ Nat : Type => b (Nat -> Nat) (a Nat) printNatT : NatT -> IO ()printNatT n = print (n Nat (+ 1) 0) main : IO ()main = do printNatT (exp two two)