This idea keeps floating in my mind and I would like to know if it's already described somewhere or if it at least could work:
Let's say we typecheck language with this constraint-solving mechanism that GHC uses - create unification variables for values, run through syntax tree inferring some constraints, solve constraints, fill in solved types in place of variables. Now, what if one value had more of these - what if it had multiple types, in different, parallel universes? What I mean by this is that there would be multiple unification variables for same value in different universes, with separate inference pass and unification mechanism which could be part of compiler or maybe a plugin - they would share the same typechecker "framework" with normal Type universe and could have "runtime proofs" (similar to coercions or dictionaries), but they could check different properties about code, parallel to normal types. For example, I could have universe of multiplicities, where these custom extension would check whether number of uses of some value corresponds to it's inferred/assigned multiplicity. Or maybe universe of subtyping relations - imagine we created universe data Optic = Getter Type Type | Setter Type Type Type | Lens Type Type Type Type | ... where unification would respect subtyping relations between optics and emit conversions between representations as runtime proofs - similarly to Type signatures, we could have Optic signatures, e.g. telling that view expects optic of type Getter (Type type could be something monomorphic and opaque to not get into way).
Motivation for this is some sort of extensibility in type system - currently, when you want to introduce additional property to types, you usually do so by indexing all relevant types over it, which is backwards-incompatible solution that doesn't scale indefinitely - with sort of parallel model, I could define additional properties for values I care about and infer some dummy types for other values in backwards-compatible way.
This idea keeps floating in my mind and I would like to know if it's already described somewhere or if it at least could work:
Let's say we typecheck language with this constraint-solving mechanism that GHC uses - create unification variables for values, run through syntax tree inferring some constraints, solve constraints, fill in solved types in place of variables. Now, what if one value had more of these - what if it had multiple types, in different, parallel universes? What I mean by this is that there would be multiple unification variables for same value in different universes, with separate inference pass and unification mechanism which could be part of compiler or maybe a plugin - they would share the same typechecker "framework" with normal
Typeuniverse and could have "runtime proofs" (similar to coercions or dictionaries), but they could check different properties about code, parallel to normal types. For example, I could have universe of multiplicities, where these custom extension would check whether number of uses of some value corresponds to it's inferred/assigned multiplicity. Or maybe universe of subtyping relations - imagine we created universedata Optic = Getter Type Type | Setter Type Type Type | Lens Type Type Type Type | ...where unification would respect subtyping relations between optics and emit conversions between representations as runtime proofs - similarly toTypesignatures, we could haveOpticsignatures, e.g. telling thatviewexpects optic of typeGetter(Typetype could be something monomorphic and opaque to not get into way).Motivation for this is some sort of extensibility in type system - currently, when you want to introduce additional property to types, you usually do so by indexing all relevant types over it, which is backwards-incompatible solution that doesn't scale indefinitely - with sort of parallel model, I could define additional properties for values I care about and infer some dummy types for other values in backwards-compatible way.