RE: [Haskell-cafe] handling rank 2 types
In a type system like MLF, your original code may type check. 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. It is rather about functions with classic rank-1 types. To see this, insert $ for the application of Empty: fooBar :: [v] -> Empty fooBar l = Empty $ (map no l) where no :: a -> a' no x = error "element found" You get the same type error as for the original monadic code. What you could do is define a suitably typed application operator (likewise, a suitably typed liftM). (With MLF the various types would be admitted by a more general type.) 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 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'"? Parametric polymorphism seems to suggest that we can't do much. You can observe the length of the list. That's it, more or less. Why not store the length directly rather than having this superficially polymorphic list? I am a little bit lost. You wonder how you can generally solve this sort of problem? - You seem to spot the wrapping approach: wrap foralls and unpack at application time. This makes particularly sense for polymorphic *functions*. - The other approach is to use consistently rank-2 combinators. I probably don't get what you try to do. Ralf
-----Original Message----- From: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe- bounces@haskell.org] On Behalf Of Andrew Pimlott Sent: Thursday, November 03, 2005 8:35 PM To: haskell-cafe@haskell.org Subject: [Haskell-cafe] handling rank 2 types
I am trying to use a rank 2 type to enforce a condition on a data structure. For the purpose of this message, I am trying to ensure that a list is empty (ignoring the possibility of bottom elements):
{-# OPTIONS -fglasgow-exts #-} import Control.Monad newtype Empty = Empty (forall a. [a])
I want a function
listToEmpty :: [v] -> IO Empty listToEmpty l = liftM Empty (mapM no l) where no :: a -> IO a' no x = fail "element found"
But this gives a "less polymorphic" error. I think the problem is that ghc will not instantiate the "a'" in "IO a'" as a higher-rank type because it occurs within a type contructor. I believe this is the restriction referred to at the end of 7.4.9[1]. If I instead write
uncheckedListToEmpty :: [v] -> Empty uncheckedListToEmpty l = Empty (map no l) where no :: a -> a' no x = error "element found"
it compiles, because "v'" can be instantiated as "forall v. Rule v", and even pass through map with the higher-rank type.
Is there any way to make ghc accept the first definition? I found this workaround:
newtype Any = Any { unAny :: forall a. a } listToEmptyAny :: [v] -> IO Empty listToEmptyAny l = liftM (\l -> Empty (map unAny l)) (mapM no l) where no :: a -> IO Any no x = fail "element found"
But needing a newtype wrapper Empty was bad enough; do I really need one for every intermediate result (that is inside another type constructor) as well? I could probably define a generic family of wrappers
newtype Forall = Forall (forall a. a) newtype Forall1 c1 = Forall1 (forall a. c1 a) newtype Forall2 c1 c2 = Forall2 (forall a. c1 c2 a) ...
But I would still have to use them everywhere. Any other tricks?
Andrew
[1] http://haskell.org/ghc/docs/latest/html/users_guide/type- extensions.html#universal-quantification
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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
participants (2)
-
Andrew Pimlott -
Ralf Lammel