An implementation of System F in JavaScript, for my practicing and learning it and its treatment.
git clone https://github.com/susisu/system-f-js-impl.git
cd system-f-js-impl
npm install
npm startt ::= -- term
x -- variable
fun x: T. t -- abstraction
t t -- application
fun2 X. t -- type abstraction
t [T] -- type application
T ::=
X -- type variable
T -> T -- arrow type (for abstractions)
forall X. T -- universal type (for type abstractions)
Variable X; -- assumes type variable X
Axiom x: T; -- assumes variable x: T (synonym: Hypothesis)
Define x = t; -- defines x = t
Theorem x: T = t; -- checks t has a type T and defines x = t (synonyms: Lemma, Corollary)
Reduce t; -- performs full beta-reduction on t
Print x; -- prints term bound to x
Clear; -- clears the context
> Variable False;
False is assumed.
> Axiom ex: forall X. False -> X;
ex: forall X. False -> X is assumed.
> Axiom dne: forall X. ((X -> False) -> False) -> X;
dne: forall X. ((X -> False) -> False) -> X is assumed.
> Theorem peirce: forall A, B. ((A -> B) -> A) -> A
| = fun2 A.
| fun2 B.
| dne [((A -> B) -> A) -> A] (
| fun H: (((A -> B) -> A) -> A) -> False.
| H (
| fun H0: (A -> B) -> A.
| H0 (
| fun H1: A.
| ex [B] (
| H (
| fun H2: (A -> B) -> A.
| H1
| )
| )
| )
| )
| );
peirce: forall A. forall B. ((A -> B) -> A) -> A is defined.
> Print peirce;
peirce: forall A. forall B. ((A -> B) -> A) -> A
= fun2 A. fun2 B. dne [((A -> B) -> A) -> A] (fun H: (((A -> B) -> A) -> A) -> False. H (fun H0: (A -> B) -> A. H0 (fun H1: A. ex [B] (H (fun H2: (A -> B) -> A. H1)))))
> Clear;
> Print peirce;
Reference Error at (line 1, column 1):
unbound variable: peirce
> Define s = fun2 A, B, C. fun x: A -> B -> C, y : A -> B, z : A. x z (y z);
s: forall A. forall B. forall C. (A -> B -> C) -> (A -> B) -> A -> C is defined.
> Define k = fun2 A, B. fun x: A, y : B. x;
k: forall A. forall B. A -> B -> A is defined.
> Define i = fun2 A. fun x: A. x;
i: forall A. A -> A is defined.
> Reduce fun2 X. fun x: X. s [X] [X] [X] (k [X] [X]) (i [X]) x;
fun2 A. fun a: A. a