| // A nano dependent type-checker featuring inductive types via self encodings. | |
| // All computation rules are justified by interaction combinator semantics, | |
| // resulting in major simplifications and improvements over old Kind-Core. | |
| // Specifically, computable annotations (ANNs) and their counterpart (ANN | |
| // binders) and a new self encoding based on equality (rather than dependent | |
| // motives) greatly reduce code size. A more complete file, including | |
| // superpositions (for optimal unification) is available on the | |
| // Interaction-Type-Theory repository. | |
| // Credits also to Franchu and T6 for insights. |
Majority of the resources I used to build Tucan, my toy optimizing compiler in Rust. This list is not complete but most of the things listed here are things I really read through and used.
| (menhir | |
| (modules parser)) | |
| (ocamllex lexer) | |
| (executable | |
| (name ex)) |
| (** "Landin's Knot" - implements recursion by backpatching *) | |
| let landins_knot f = | |
| let r = ref (fun x -> assert false) in | |
| let fixedpoint = f (fun x -> !r x) in | |
| r := fixedpoint; | |
| fixedpoint | |
| let factorial = | |
| let g f x = | |
| if x = 0 then |
L1 cache reference ......................... 0.5 ns
Branch mispredict ............................ 5 ns
L2 cache reference ........................... 7 ns
Mutex lock/unlock ........................... 25 ns
Main memory reference ...................... 100 ns
Compress 1K bytes with Zippy ............. 3,000 ns = 3 µs
Send 2K bytes over 1 Gbps network ....... 20,000 ns = 20 µs
SSD random read ........................ 150,000 ns = 150 µs
Read 1 MB sequentially from memory ..... 250,000 ns = 250 µs