On Thu, Nov 03, 2005 at 11:57:49PM -0800, Ralf Lammel wrote:
Let's do an experiment. We replace the IO monad by the Id(entity) monad. We actually replace the Id newtype also to become true type-level identity. So we get:
-- -- This is like your 2nd say unchecked... sample --
fooBar :: [v] -> Empty fooBar l = Empty (map no l) where no :: a -> a' no x = error "element found"
But the problem is not about "a higher-rank type occurring with a type constructor", as you guess.
I thought my explanation sounded fishy. Someone else explained this to me off-list as well.
It is rather about functions with classic rank-1 types. ... What you could do is define a suitably typed application operator (likewise, a suitably typed liftM). ... In the non-monadic example, we need:
-- Use app instead of ($) app :: ((forall a. [a]) -> c) -> (forall b. [b]) -> c app f x = f x
Ok, but this would have to be rewritten for different kinds: app1 :: ((forall a. c1 a) -> c) -> (forall b. c1 b) -> c app1 f x = f x app2 :: ((forall a. c1 c2 a) -> c) -> (forall b. c1 c2 b) -> c app2 f x = f x ... Furthermore, I don't believe it works for me. I would need something like liftM' :: Monad m => (forall a. [a] -> c) -> m (forall b. [b]) -> m c liftM' f x = ??? First, the type is illegal: "you cannot make a forall-type the argument of a type constructor". Second, even if it were, I would need versions of the monad operators with custom types to implement it, eg bind :: Monad m => m (forall a. [a]) -> ((forall b. [b]) -> m c) -> m c Or am I wrong? An alternate (and legal) signature for liftM' is liftM' :: Monad m => (forall a. [a] -> c) -> (forall b. m [b]) -> m c but to implement this, I think I would need bind :: Monad m => (forall a. m [a]) -> ((forall b. [b]) -> m c) -> m c I tried implementing this just for Maybe: bindMaybe :: (forall a. Maybe [a]) -> ((forall b. [b]) -> Maybe c) -> Maybe c bindMaybe x f = case x of Just x' -> f x' Nothing -> Nothing But as expected, it doesn't typecheck, and AFAICT it shouldn't. So my conclusion is that writing my own higher-ranked library wouldn't work; I would still need newtype wrappers.
BTW, what operations are we supposed to perform on the content of Empty; what's the real purpose for introducing this independent type variable "a'"?
Suppose instead newtype NoRight = NoRight (forall a. [Either Int a]) An alternative might be data No type NoRight = [Either Int No] But the first version I can use directly (after unwrapping NoRight) as an [Either Int Int], [Either Int String], etc. My real purpose is to enforce that a logical statement has no variables. Andrew