Open treeowl opened 8 years ago
This would be nice. I came here to ask for a Set.coerce
but I don't know which is better.
It's a very unsatisfying situation, because ideally we could just use coerce
and GHC would throw an error in the rare case that we didn't just derive Ord
somewhere, and so we could get something that's safer than mapMonotonic
for this use-case.
@jberryman, we can offer these rules while maintaining a "standard Haskell" API. For coercing, we'd want
setCoercion :: Coercible a b => Coercion (Set a) (Set b)
-- and/or
quantCo :: ((forall a b. Coercible a b => Coercible (Set a) (Set b)) => r) -> r
Unfortunately, the nasty way type roles work for data
means we need unsafeCoerce
for the former and also mean I have no idea how if at all to implement the latter. Will you be at Haskell DC on Wednesday?
Yeah assumed, but wasn't totally sure if this was guaranteed to be safe (at least as safe as mapMonotonic
):
setCoerce :: Coercible a b => Coercion (Set a) (Set b)
setCoerce = unsafeCoerce
(And my first comment was a little jumbled; if it wasn't clear I meant that it's a bit of a shame that setCoerce
can't be made to be safer than mapMonotonic coerce
.)
Will you be at Haskell DC on Wednesday?
No, but I'd love to come up for one sometime if I can. Just subscribed to the meetup group.
@jberryman What goes wrong with the safe version, as in
setCoercion :: Coercible a b => Coercion (Set a) (Set b)
setCoercion = Coercion
(defined within a module that has access to Set
's constructors, of course)?
@jberryman that's definitely not safe. Consider
newtype DInt = D {getDInt :: Int} deriving (Eq)
instance Ord DInt where D x < D y = y<x
Then coerce
is not monotonic, and thus unsafeCoercing
the maps would give a corrupted data structure.
But I'm not sure if that goes off on a tangent WRT to the question you meant to discuss here.
@jberryman What goes wrong with the safe version, as in
setCoercion :: Coercible a b => Coercion (Set a) (Set b) setCoercion = Coercion
(defined within a module that has access to
Set
's constructors, of course)?
@dmwit, the type checker will reject that thanks to the nominal
role. The zero-cost coercion designers took a freebie that wasn't really so free. They liked the idea of
F's parameter has a representational role |-
Coercible (F a) (F b) => Coercible a b
F's parameter has a nominal role |-
Coercible (F a) (F b) => a ~ b
These can't work for newtype
s, because it's just so obviously useful to be able to coerce them wildly when their constructors are in scope. But they figured they'd enforce the rule that data
inherently and unconditionally has the role given in the role signature, giving them what they wanted. But that means we can't safely coerce nominal
data
even in the defining module.
Right, and the reason nominal
data can't be safely coerced is precisely that it would allow mayhem like non-monotonic coerce destroying a set tree's invariant.
(If it's not obvious already, I think that they were wrong to take that "freebie" and that it should be removed. It's not actually very useful and it gets in the way of a variety of potential good things.)
(Alternatively, there could be a "soft" role signature and a "hard" role signature, where only the latter enables the backwards reasoning.)
mapMonotonic coerce = coerce
andmapKeysMonotonic coerce = coerce
, or so.