[Haskell-cafe] Cons of -XUndecidableInstances

[wren ng thornton]

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:

     instance
         forall f.
         ( Show (Mu f) => Show (f (Mu f)) )
         => Show (Mu f)
         where...

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.

-- 
Live well,
~wren