4 ms·

Related: https://treecalcul.us https://treecalcul.us https://github.com/barry-jay-personal/tree-calculus/blob/master/tree_book.pdf https://github.com/barry-jay

by 4ad 2y ago

Related: https://treecalcul.us https://treecalcul.us https://github.com/barry-jay-personal/tree-calculus/blob/master/tree_book.pdf https://github.com/barry-jay-personal/tree-calculus/blob/mas... TBH, I am not sure I understand how this is different from Tree Calculus. Is it just the addition of dependent types?

jbhn 2y ago
Reflections in Tree Calculus work differnt from lisp quote/unqote used here. It is a hunch, but I think Tree Calculus can implement this (if it is sound) (book pg 64 ff on quote), but not vice-versa. As far as I know there is no Tree Calculus with (dependent) types, because types in Tree Calculus work different from main stream type theory (you internalize the type checker using reflection (see book pg 58), a bit like I did here with scheme: https://github.com/JanBessai/tcscheme https://github.com/JanBessai/tcscheme).