3 ms·
This is an old yarn distinguishing sets and types, extrinsic and intrinsic, "run time" and "compile time". The idea of a runtime procedure `?- atom(_)` which d
by tel 5y ago
This is an old yarn distinguishing sets and types, extrinsic and intrinsic, "run time" and "compile time".
The idea of a runtime procedure `?- atom(_)` which determines `true.` or `false.` is fundamentally an extrinsic property, thus "set like".
Intrinsically defined objects are defined through (possibly inductive) construction or (possibly coinductive) destruction rules.
Typically a notion of set arises from having some larger universe of things and restricting them via predicates. The notion of types arises from having a system of building (co)inductive definitions and then utilizing that system. Sets are thus, in a sense, fundamentally based on a closed world (said universe) and types an open world (each new utilization of the rules system introduces a novel type).