If we get rid of the higher-order nested types, then we get better type roles:
newtype Zero a = Zero a
data Succ k rk = Succ {-# UNPACK #-} !(Tree k rk) rk
data Tree k rk = Tree !k rk
data Forest k rk
= Nil
| Skip (Forest k (Succ k rk))
| Cons {-# UNPACK #-} !(Tree k rk) (Forest k (Succ k rk))
newtype BinomHeap k a = BH (Forest k (Zero a))
type role BinomHeap nominal representationalThe only problem is that the GADT-style stuff for unordered operations gets considerably less pretty. Implementing unsafe key maps and normal maps and unordered traversals seems to require something like
data Natty k1 k2 a1 a2 rk1 rk2 where
Zeroy :: Natty k1 k2 a1 a2 (Zero a1) (Zero a2)
Succy :: !(Natty k1 k2 a1 a2 rk1 rk2) -> Natty k1 k2 a1 a2 (Succ k1 rk1) (Succ k1 rk2)
that relates the list-of-trees type for the origin type to that of the destination type.
Is it worth the pain to get the better type role?
If we get rid of the higher-order nested types, then we get better type roles:
The only problem is that the GADT-style stuff for unordered operations gets considerably less pretty. Implementing unsafe key maps and normal maps and unordered traversals seems to require something like
that relates the list-of-trees type for the origin type to that of the destination type.
Is it worth the pain to get the better type role?