RE: Strange error in show for datatype
| > My claim was that | > | > forall a. Show a => T | > | > could be implemented by passing a bottom dictionary for Show. | | Excuse me, but Jan-Willem Maessen has already shown that this | implementation can give unexpected results. Yes, I was quite wrong about that. How embarassing. But there's still something lurking there. Consider: data T a = T1 Int | T2 a It's clear that (T1 Int) has no a's in it, not even bottom. Mark Shields and ruminated in the corridor about a kind system to make this apparent. That is, T1 would have type T1 :: forall a::Pure . Int -> T a Then if we see (forall a::Pure. Show a => <type>) we're justified in fixing a to Empty. You need a sub-kinding system to make this work, so the cost has just gone up. My implemention mood has suddenly past. Isn't laziness wonderful? Simon
Simon Peyton-Jones wrote:
Consider:
data T a = T1 Int | T2 a
It's clear that (T1 Int) has no a's in it, not even bottom. Mark Shields and ruminated in the corridor about a kind system to make this apparent. That is, T1 would have type
T1 :: forall a::Pure . Int -> T a
Then if we see (forall a::Pure. Show a => <type>) we're justified in fixing a to Empty.
I think that even with this kind system, we can't fix it 'a' to Empty. For example, the empty list constructor would get type: [] :: forall (a::Pure) . [a] and as Koen showed, we still can't fix the 'a' to Empty. -- Daan.
participants (2)
-
Daan Leijen -
Simon Peyton-Jones