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