Show and Tell - my javascript attempt at Type Theory!

Stream: new members

[Mr Proof]

People always say, that to understand something fully you should be able to create the thing yourself. With that in mind, in order to understand Lean type theory, I attempted to make something similar using Javascript.

If anyone is interested in my (incomplete, slightly buggy) implementation of a Lean-like language the link is here. I was going to wait until it was more complete or fixed all the bugs, but that will probably never happen.

It consists for two parts, the typetheory.js which defines the basic languages and the definitions.js which has lots of mathematical statements (equivalent to the mathlib - but with basically all the statements are unproved).

The main point of it was really to (1) try to understand in my own mind how type theory works and (2) try to experiment with making it look nice with latex and (3) concentrate on more physics like math.

Some thing I learned while making it was: (1) It seems quite necessary to deal with natural number arithmetic using BigNum not storing it as S(S(S(....)) for example, even though that makes the language a little "less pure". (2) Same probably goes for lists too. (3) Dealing with tensor/spinor fields abstractly is very difficult since it matters which order we curry the variables and indices. And the indices themselves can be permuted by a group. Hence why probably there is no really good abstract way of dealing with tensors - the Einstein summation is prettiest but hard to translate directly to type theory.

Some things not implemented include: (1) The "match" syntax - which is probably very important.

I'm not much sure what I may do with this implementation if I ever fix all the bugs.

Feel free to ask any questions about it or suggest improvements. Or if you have implemented your own type theory let me know and I will try it out.

[Matt Diamond]

Is there a separate GitHub repo for the Javascript library? I can view the source code here, but I was wondering if that was compiled from a separate project.

[Matt Diamond]

I'm also surprised that you didn't write it in Typescript, especially since it's about type theory! (Or is the Javascript file just the build output from a Typescript project?)

[Mr Proof]

That's basically it. The only outside files are the mathjax libraries to do the latex. If you look at one of the doc pages you will see the js references at the top. It's certainly not feature complete and has bugs. (Mainly it messes up some types when doing replacements). I see this more as something people might use for inspiration rather than something useful or reliable.

Yeah, Typescript should probably have been used. But of course the types here are just javascript objects in a tree structure. Typescript is of course not dependently typed.

Also, the github webpage seems to be really slow today for some reason. Not sure why.