strangemonad
commented
6 years ago Pullbacks / fiber products might be a way to define abstract concepts more specifically along different dimensions of interpretation of the type.
E.g. and Instant has an interpretation along a “granularity” dimension and along a “extents” dimention (and no other). The pullback of these is the set of all representable instants.
By pasting, if one of the dimensions is it self a fiber product, we can continue “refining”
Eg. maybe 2 definitions of Instant. It should be possible to just define mappings in both directions. But we need to capture the semantic sense of the object (e.g. in the case of 2 different instants, the granularity and extent).
see PFPL 17.4 (representation independence of existential / abstract types and solving semantic type equations). The question becomes, what domain to interpret things in (e.g. for the granularity and extent of 2 instant types Instant({seconds:long, nanos:long}) MyInstant({millis:long}).
1) Should conversion with known loss of precision ever be allowed? eg: instant.toMyInstantWithLoss() (lots of potential right / wrong ways to round and all are application specific e.g. truncate, even odd, redistribute the lost accuracy etc etc) 2) MyInstant can always be converted into Instant (just capture this as a subtype / type refinement problem)? 3) Not always possible (e.g. UTF8 string to ASCII or LATIN-1 string or some other encoding that can't express all the unicode code points)