Hidden types and scope
Hello cafe, While writing some code, I stumbled upon quite an interesting behavior. See the code example below. ------------------------------------------------------------- {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE RankNTypes #-} data Wrapper = forall m. Monad m => Wrapper { runAction :: forall a. m a -> IO a , someAction :: String -> m () } newtype MyIO a = MyIO { runIO :: IO a } deriving (Monad) ex :: Wrapper ex = Wrapper runIO (\s -> MyIO (putStrLn s)) {- This doesn't work -} --main :: IO () --main = do let Wrapper r a = ex -- r (a "Hello") {- This works -} main :: IO () main = case ex of Wrapper r a -> r (a "Hello") ------------------------------------------------------------- The idea is to hide the exact type `m` used in the wrapper, making the wrapper somewhat opaque to the user, while exposing some functionality and making sure that using `runAction` with the rest of the members of Wrapper is type-safe and `m` is always the same type within one instance of Wrapper. The problem that I ran into is that the first version of `main` doesn't compile with the following error: • Couldn't match expected type ‘p’ with actual type ‘forall a. m a -> IO a’ because type variable ‘m’ would escape its scope This (rigid, skolem) type variable is bound by a pattern with constructor: Wrapper :: forall (m :: * -> *). Monad m => (forall a. m a -> IO a) -> (String -> m ()) -> Wrapper, in a pattern binding at wildcards.hs:18:15-25 • In the pattern: Wrapper r a In a pattern binding: Wrapper r a = ex In the expression: do let Wrapper r a = ex r (a "Hello") This is repeated for every member of Wrapper that is matched in a let expression. However, if let expression is replaced with case, everything builds and works just fine. Is there a way to make it work with let expressions? That way the code is a lot cleaner, especially with RecordWildCards involved.
A followup question. What is the reason case and let expressions are treated differently in this case? I can see the error message saying about the type variable escaping its scope, but I don't understand how exactly this can happen with let.
What is the reason case and let expressions are treated differently in this case
Please check the section "7.4.5.4. Restrictions section" in https://downloads.haskell.org/~ghc/7.6.3/docs/html/users_guide/data-type-ext... It says,
In general, you can only pattern-match on an existentially-quantified constructor in a case expression or in the patterns of a function definition. The reason for this restriction is really an implementation one. Type-checking binding groups is already a nightmare without existentials complicating the picture. Also an existential pattern binding at the top level of a module doesn't make sense, because it's not clear how to prevent the existentially-quantified type "escaping". So for now, there's a simple-to-state restriction. We'll see how annoying it is.
On 10/07/19 9:26 PM, Lana Black wrote:
A followup question. What is the reason case and let expressions are treated differently in this case? I can see the error message saying about the type variable escaping its scope, but I don't understand how exactly this can happen with let. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
On 10/07/2019 16:03, Sandeep.C.R via Haskell-Cafe wrote:
What is the reason case and let expressions are treated differently in this case
Please check the section "7.4.5.4. Restrictions section" in https://downloads.haskell.org/~ghc/7.6.3/docs/html/users_guide/data-type-ext...
It says,
In general, you can only pattern-match on an existentially-quantified constructor in a case expression or in the patterns of a function definition. The reason for this restriction is really an implementation one. Type-checking binding groups is already a nightmare without existentials complicating the picture. Also an existential pattern binding at the top level of a module doesn't make sense, because it's not clear how to prevent the existentially-quantified type "escaping". So for now, there's a simple-to-state restriction. We'll see how annoying it is.
Thank you! That explains it.
Am 10.07.19 um 18:03 schrieb Sandeep.C.R via Haskell-Cafe:
What is the reason case and let expressions are treated differently in this case
Please check the section "7.4.5.4. Restrictions section" in https://downloads.haskell.org/~ghc/7.6.3/docs/html/users_guide/data-type-ext...
It says,
In general, you can only pattern-match on an existentially-quantified constructor in a case expression or in the patterns of a function definition. The reason for this restriction is really an implementation one. Type-checking binding groups is already a nightmare without existentials complicating the picture. Also an existential pattern binding at the top level of a module doesn't make sense, because it's not clear how to prevent the existentially-quantified type "escaping". So for now, there's a simple-to-state restriction. We'll see how annoying it is.
FWIW, I personally do find the restriction pretty annoying (even though by now I am quite used to it). In some cases one can work around it by using pattern guards instead of let/where, since these are also exempt. Cheers Ben
You may need to study skolems / rank-N types. The exact scope of the "IO"
is inside the Wrapper, and nowhere else; so using it in let at all allows
it to be visible outside its scope. With the case expression, it can be
visible anywhere in the case alternative that pattern matches the Wrapper
without it necessarily escaping the scope (you could explicitly leak it,
but it will raise the same error about it escaping in that case).
GADTs are a way to get this same case matchung behavior, but it still
doesn't help you with this; you are asking that the compiler ignore the
rank of the type variable and make it visible outside its scope so that you
can use let instead of case, and ghc will not let you do this.
On Wed, Jul 10, 2019 at 11:57 AM Lana Black
A followup question. What is the reason case and let expressions are treated differently in this case? I can see the error message saying about the type variable escaping its scope, but I don't understand how exactly this can happen with let. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
-- brandon s allbery kf8nh allbery.b@gmail.com
participants (4)
-
Benjamin Franksen -
Brandon Allbery -
Lana Black -
Sandeep.C.R