Hidden types and scope

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

Hidden types and scope

Lana Black
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.
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Hidden types and scope

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.
Reply | Threaded
Open this post in threaded view
|

Re: Hidden types and scope

Haskell - Haskell-Cafe mailing list
 >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-extensions.html

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.
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Hidden types and scope

Brandon Allbery
In reply to this post by Lana Black
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 <[hidden email]> 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.


--
brandon s allbery kf8nh

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Hidden types and scope

Lana Black
In reply to this post by Haskell - Haskell-Cafe mailing list
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-extensions.html 
>
>
> 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.
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Hidden types and scope

Ben Franksen
In reply to this post by Haskell - Haskell-Cafe mailing list
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-extensions.html
>
>
> 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

_______________________________________________
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.