erisco [11:25 AM]
@natefaubion are there any special considerations you have in Variant wrt duplicate labels?
it seems only the first label is constructable
which also seems important (to have some convention) because the only RTTI is the label, so of course (foo :: Int, foo :: String) would not want to be confused
not sure what the Nub convention is but if it keeps first labels, that is a free Variant conversion
natefaubion [11:48 AM]
I’m not sure what (foo :: Int, foo :: String) means wrt variant
I know you might intuitively think foo is inhabited by both Int and String at runtime, but no, that’s not really what it means
Something like polymorphic variants in OCaml would be equivalent to prefixing the label with a module name, ("Run.State" :: STATE Int | r)
@erisco duplicate labels are useful, without them purescript-checked-exceptions wouldn’t be possible
wrt Variant duplicate labels are more like scope shadowing
erisco [11:59 AM]
I don’t intuitively think that. Why are they essential to checked exceptions?
natefaubion [12:01 PM]
for example, handleException { foo: \e -> throwFoo e } that is, you throw the same label in the context of handling. At some point it must unify with (foo :: Foo, foo :: Foo | r)
erisco [12:02 PM]
what I intuitively think is that duplicate labels are nonsense for Variant, but given their presence, the convention is only the first label is constructable
you’ve been careful of that in several places, such as expand
if you reversed the first two parameters of Union then it would be wrong
natefaubion [12:03 PM]
Yes, the first occurrence represents the current scope
So by being on the left of Union, it ensures it’s the current scope
erisco [12:04 PM]
what is scoped about it?
you can peel off a label with on, and then handle the remaining cases, is that what you mean?
natefaubion [12:04 PM]
variant elimination just doesn’t work the way you expect without duplicate labels
What it means, is that once you eliminate a label, you effectively can’t reintroduce that label again
so for exception handling, that means you can only handle a particular kind of exception once in your program
which pushes your exception handling to be global (edited)
Eff (err :: EXCEPTION | eff) had this problem before we allowed duplicate labels
erisco [12:10 PM]
seems like a subtle point about the type system which I’m not going to try and fully understand at the moment
I am looking at several things but one simple one is that removing duplicates (keeping the first) should be a free conversion on Variant
natefaubion [12:12 PM]
You should be able to Nub yes, but in practice I’ve never seen this come up as a requirement
erisco [12:12 PM]
it can clean up types
natefaubion [12:13 PM]
Do you have examples where this arises in practice?
I think this only becomes a thing if you are using closed variants
erisco [12:13 PM]
no, because I am working on checked exceptions which are not used in practice yet because I am still developing them
well, guess what, it involves closed variants 
natefaubion [12:15 PM]
In my experience closed variants kind of end up fighting the current
Things no longer “just work” and you have to do a lot of massaging the types
erisco [12:15 PM]
it isn’t debatable for this particular scenario, i.e. anything else would be wrong
I am going beyond the typical try/catch to accommodate more implementations… you shall see
natefaubion [12:16 PM]
I’ll be interested to see what you’re up to 
erisco [12:17 PM]
well, I’ve said it before. I have realised that catching can be done in more than one way (as have you, as you have at least two paradigms for catching)
and if you ponder some more you realise that catchers are interesting objects themselves
and that is where closed rows happen, because a catcher only catches some exceptions
erisco [12:29 PM]
@natefaubion this is a conversion I am working with if you’d like to weigh in https://github.com/natefaubion/purescript-variant/issues/32
I think it is a more powerful idea of contract