Sean Leather wrote: > inside :: ((forall a. W (t a))-> W (forall a. (t a))) > --inside (W x) = W x -- (a) FAILS > --inside = W . unW -- (b) FAILS > inside x = W (unW x) -- (c) WORKS > > Are there any pointers for developing a better understanding or > intuition of this?
Usually, making type arguments explicit helps: that is, assume that each polymorphic value is actually a function expecting a type (the a in forall a. ...) and returning the value related to that type. The last 'inside' definition becomes: inside x = W (\type -> unW (x type)) Note that we do not know at this time what will be the actual "type" above. But that's OK, since we can return a type-lambda. Instead, pattern matching desugars to: inside x = case x of ... But wait! x is a function (because it's polymorphic) and we can not pattern match on that! And, at this time, we do not know the type-argument for x. So we are stuck. Also, type-lambdas and type-arguments are hard to insert in W . unW . For more tricks with type-lambdas, look up "System F". Hope this helps, Zun. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe