3 ms·
The key of the idea is you're not asserting that predicates on values are true, you're recognizing whether a value (of a type with few guarantees) conforms to t
by lalaithion 4y ago
The key of the idea is you're not asserting that predicates on values are true, you're recognizing whether a value (of a type with few guarantees) conforms to the guarantees of a type (implicitly, a type with more guarantees), and transforming the value into a value of the output type.
Parsing might not be the right word, but it's definitely an example of the above; we transform a string into a tree of tagged nodes.
- aatd86 4y agoYes, I think another simpler way to do it is to have a set theoretic interpretation of types with subtyping. In which case, we can check that a variable can be type-asserted to a given subtype. A (sub)type being a set of propositions (i.e. defines a set of values).