2 ms·
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
by weberc2 9y ago
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.
- naasking 9y ago> 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.