Re:Collapsing towers of interpreters [pdf]
by weberc2 on Monday November 06, 2017 @01:26PM
(#15637565)
Types (or "type expressions") are expressions whose type is type. In other words, types are higher order expressions. It's a poor definition or discipline that doesn't capture this basic concept.
[ Parent
| on HN ]
Re:Collapsing towers of interpreters [pdf]
by naasking on Monday November 06, 2017 @11:12PM
(#15641030)
> Types (or "type expressions") are expressions whose type is type.
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.