3 ms·
I'm curious how you implement associated types and equivalences between them. In the most general case, this allows encoding an arbitrary finitely-presented mon
by slavapestov 4y ago
I'm curious how you implement associated types and equivalences between them. In the most general case, this allows encoding an arbitrary finitely-presented monoid in the type system, and the word problem on finitely-presented monoids is undecidable. However, you mention your type checker is Turing-complete.
- zesterer 4y agoYep, this is the case: the type-checker allows arbitrary computation to occur at compilation time. You can see some of that here, where I've implemented peano arithmetic/addition/multiplication/branching using the type system: https://github.com/zesterer/tao/blob/master/examples/type-astronomy.tao https://github.com/zesterer/tao/blob/master/examples/type-as... . I've not yet had the time or mental fortitude to implement something more non-trivial like N-queens or a Brainfuck interpreter, but perhaps eventually!