[Haskell-cafe] Cons of -XUndecidableInstances
wren ng thornton
wren at freegeek.org
Tue Jun 7 22:49:41 CEST 2011
On 6/7/11 1:01 PM, James Cook wrote:
> On Jun 7, 2011, at 12:43 PM, MigMit wrote:
>> wren ng thornton wrote:
>>> One particularly trivial example that comes to mind is:
>>> newtype Mu f = Mu (f (Mu f))
>>> instance Show (f (Mu f)) => Show (Mu f) where
>>> show (Mu x) = "Mu (" ++ show x ++ ")"
>>> -- Or however you'd like to show it
>> Ehm, that does look like poor design.
>> Sure you don't mean "Mu f can be printed if and only if f (Mu f) can
>> be printed". What you probably mean is "if f transforms printable
>> things to printable things, then Mu f is a printable thing". And you
>> CAN express just that:
> Actually, I would argue that the former _is_ what is meant. It's a
> weaker condition than the latter and it is the necessary and sufficient
> condition to define the instance - one of the steps involved in
> formatting a value of type "Mu f" is to format a value of type "f (Mu
> f)". It doesn't actually matter whether "forall x. Show x => Show (f x)"
> holds in general.
Indeed. Often the fact that (forall x. Show x => Show (f x)) holds will
serve to prove that Show (f (Mu f)), but there's no reason why the more
stringent proof is a requirement. The necessary and sufficient condition is:
( Show (Mu f) => Show (f (Mu f)) )
=> Show (Mu f)
Which isn't directly expressible in Haskell. And even if we could write
it, it wouldn't mean what it ought to mean; because the typeclass
resolution system commits to an instance once the head matches, rather
than viewing the context as preconditions for matching the head. Thus,
there's no way to pass in an implication like that; it's equivalent to
requiring both Show (Mu f) and Show (f (Mu f)). And since the former is
trivially satisfied, we only need to specify the need for Show (f (Mu f)).
>> type ShowD a = forall p. (forall x. Show x => p x) -> p a
While I don't shy away from RankNTypes, I don't see that this really
buys us anything. UndecidableInstances is easily supportable, higher
rank polymorphism takes a bit of work and therefore reduces portability.
More information about the Haskell-Cafe