[Haskell-cafe] handling rank 2 types
Andrew Pimlott
andrew at pimlott.net
Fri Nov 4 14:26:37 EST 2005
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
More information about the Haskell-Cafe
mailing list