4 ms·
You might be interested to learn that in languages like Coq with dependent types, the difference between type-level and value-level languages (almost) disappear
by benrbray 5y ago
You might be interested to learn that in languages like Coq with dependent types, the difference between type-level and value-level languages (almost) disappears! Check out the Software Foundations book [1].
[1] https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/