|
|
|
|
|
|
by benrbray
1599 days 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/ |
|
|