In that case it seems like you do want to produce the dictionary inside the if, i.e. elaborate to:
showIntOrString (if b then (5 :: Int, showIntDict) else ("hello", showStringDict))
I currently do not know how this would scale to more complex scenarios. One approach which works is to not completely erase types. We could then use a type_of operator at runtime which looks up the type-tag of the value, and dispatch to the correct type class instance based on the tag. (If we care about parametricity, then this type_of operator should not be user visible, of course). But this means that we would lose the nice performance properties of type-erasure in a language like Haskell.
I actually did a lot of literature research on the topic, but as far as I can see nobody has published on the combination of subtyping and type classes before. (By type classes I mean the coherent ones that Haskell and Rust implement. If we ignore coherence, then the problem becomes much simpler, and there is work on integrating them in languages like Scala).
1 Like
Yeah, you’re right, a simple example would be:
foo b = if b then (5 :: Int) else "hello"
bar b = show (foo b)
Now we need to be careful when we modify foo in the elaboration because it could be used by other functions. E.g. you wouldn’t want to mention Show dictionaries in foo.
Instead of keeping around all type information, it seems you could just elaborate all A \/ B types to a sum type:
foo b = if b then Left\/ (5 :: Int) else Right\/ "hello"
bar b = show\/ showIntDict showStringDict (foo b)
Or are there even more complicated types where this would not work?
1 Like
That might work, the problem for me is that this implementation strategy is in conflict with the way I think about types in algebraic subtyping. One of the central properties of algebraic subtyping is that you can always infer the principal type. This principal type is semantically unique, but not syntactically unique. (In standard Hindley-Milner type inference syntactic and semantic uniqueness coincide up to names and order of the type variables). For example, the const function \x y -> x has a unique principal type, but that type has many ways to write it, for example forall a b. a -> b -> a but also forall a. a -> Top -> a. These types are all semantically the same. For this reason, you have to employ a type simplification step which chooses a syntactic representation of the type which is the “simplest” according to some metric. This is necessarily a bit vague, but the algorithms work quite well. In the scheme you propose you make the compilation dependent on a specific chosen syntactic representation of the type. I think this can work, but it does mean that how you compile the code is now also dependent on how you simplify types.
1 Like
I believe we already do a similar thing with constraints. For example consider how these types are compiled:
foo :: (Num a, Eq a) => a -> a
bar :: Num a => Eq a => a -> a
baz :: ((Num a, Eq a), ()) => a -> a
All three are elaborated to
NumDict a -> EqDict a -> a -> a
An alternative choice would be
(# NumDict a, EqDict a #) -> a -> a
Or you could elaborate baz more syntactically to
(# NumDict a, EqDict a #) -> (# #) -> a -> a
I dug into that rabbit hole here: #20418: The () constraint should perhaps not be optimised. · Issues · Glasgow Haskell Compiler / GHC · GitLab. And note that this even has user-visible consequences.
Hmm, it seems that we cannot completely avoid the problem 
The other main argument against compiling an intersection type x \/ y as a sum type Either x y is that this leads to a lot of potential pointer indirection which is not present in the original program. I guess I would be ok with some dynamic lookup in the example we are discussing, but it should be constant and not grow with the complexity of the involved types.
That does make sense. Instead of elaborating to sum types, you could explore if it is possible to directly support union types in the runtime. Perhaps via a special tag in the infotable. And indeed if you have A \/ B \/ C then you wouldn’t want multiple layers of indirection, but just one number which indicates in which case you are. I wonder if it is always possible to make such a witness a single 64-bit integer.
After thinking some more about this there seems to be a duality between keeping around all type information (I’ll call it “address” for lack of a better term) of “plain” types (those not formed by /\ or \/) and keeping track of provenance information only in union types.
For example if you have:
data A
data B = MkB
data C
x :: B
x = MkB
y :: A \/ B
y = x
z :: B \/ C
z = x
The “provenance” approach would indicate which of the union type is used by means of a sum type:
x = MkB
y = R x
z = L x
While the “address” approach would tuple each value of a plain type with its type:
x = (MkB, B)
y = x
z = x
It seems like both could do the job. Depending on how often you use plain or union types either way might turn out to be more performant.
I think both require arbitrary amounts of additional information in the worst case. For the provenance approach that happens when you have very large union types or perhaps also when polymorphism is involved. And for the address approach that happens when you have a lot of plain types, when those are parameterised by other types, and I’d imagine polymorphic recursion would also be difficult to handle.