Every story and comment from the Hacker News API, in a layout borrowed from 2001.
A comment on Collapsing towers of interpreters [pdf]. Parent comment
This is only true in dependently typed languages. And even then, soundness requires stratifying types into universes or something similar.
> In other words, types are higher order expressions.
This isn't the meaning of higher order as it applies to programming languages or the standard isomorphism to logic.
There are no comments on this comment yet.
This is only true in dependently typed languages. And even then, soundness requires stratifying types into universes or something similar.
> In other words, types are higher order expressions.
This isn't the meaning of higher order as it applies to programming languages or the standard isomorphism to logic.