Weird defaulting on newEmptyTMVar

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

Weird defaulting on newEmptyTMVar

Ruben Astudillo
Dear list

Playing on ghci I encountered the following type

    GHCi, version 8.6.3: http://www.haskell.org/ghc/  :? for help
    Prelude> :m +Control.Concurrent.STM
    Prelude Control.Concurrent.STM> var1 <- atomically $ newEmptyTMVar
    Prelude Control.Concurrent.STM> :t var1
    var1 :: TMVar GHC.Types.Any
    Prelude Control.Concurrent.STM>

I would think `var1 :: TMVar a` as the documentation says it should.
Reading on `GHC.Types` `Any` seems to be a type family related to some
laws on `unsafeCoerce`. Can anybody explain me why is this sensible
defaulting and how to obtain the expected result?

--
-- Ruben
-- pgp: 4EE9 28F7 932E F4AD
_______________________________________________
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: Weird defaulting on newEmptyTMVar

Viktor Dukhovni
On Sun, Feb 10, 2019 at 12:24:52AM -0300, Ruben Astudillo wrote:

> Playing on ghci I encountered the following type
>
>     GHCi, version 8.6.3: http://www.haskell.org/ghc/  :? for help
>     Prelude> :m +Control.Concurrent.STM
>     Prelude Control.Concurrent.STM> var1 <- atomically $ newEmptyTMVar
>     Prelude Control.Concurrent.STM> :t var1
>     var1 :: TMVar GHC.Types.Any
>     Prelude Control.Concurrent.STM>

Much simpler:

    $ ghci
    GHCi, version 8.6.3: http://www.haskell.org/ghc/  :? for help
    Prelude> let v = Nothing
    Prelude> :t v
    v :: Maybe a
    Prelude> v <- return Nothing
    Prelude> :t v
    v :: Maybe GHC.Types.Any

This looks like let-bound polymorphism in action.  But the two types
of "Nothing" are representationally equivalent, so you can write:

    Prelude> :m + Unsafe.Coerce
    ...> case unsafeCoerce v of { Just 1 -> True; _ -> False }
    False
    ...> case unsafeCoerce v of { Just 'a' -> True; _ -> False }
    False

The case of MVars case is more complicated:

    ...> :m + Control.Concurrent.MVar
    ...> v <- newEmptyMVar
    ...> :t v
    v :: MVar GHC.Types.Any
    ...> putMVar (unsafeCoerce v) (1 :: Int)
    ...> x <- readMVar v
    ...> :t x
    x :: GHC.Types.Any
    ...> unsafeCoerce x :: Int
    1

The issues become a bit more clear if we replace the "<-" with
unsafePerformIO:
   
    ...> :m + System.IO.Unsafe
    ...> let v = unsafePerformIO newEmptyMVar
    ...> :t v
    v :: MVar a
    ...> putMVar v (1 :: Int)
    ...> let x = unsafePerformIO (readMVar v)
    ...> :t x
    x :: a

So now we seem to have an "x" that is of any type and yet is not
bottom!  We secretly know it is an Int:

    ...> unsafeCoerce x :: Int
    1

But how is GHC supposed to type check that?  So without opportunities
for type inference, and with no applicable annotations, "Any" seems
quite right, with the only way to get a value out being "unsafeCoerce".

If you want a more friendly empty MVar via the REPL, you need to
add a type annotation:

    ...> v <- newEmptyMVar :: IO (Mvar Int)
    ...> :t v
    v :: MVar Int

In compiled code the MVar's type can often be inferred from the
context in which "v" is used, and the type annotation is then
not required.

--
        Viktor.
_______________________________________________
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: Weird defaulting on newEmptyTMVar

Ian Denhardt
In reply to this post by Ruben Astudillo
Quoting Ruben Astudillo (2019-02-09 22:24:52)

> Dear list
>
> Playing on ghci I encountered the following type
>
>     GHCi, version 8.6.3: http://www.haskell.org/ghc/  :? for help
>     Prelude> :m +Control.Concurrent.STM
>     Prelude Control.Concurrent.STM> var1 <- atomically $ newEmptyTMVar
>     Prelude Control.Concurrent.STM> :t var1
>     var1 :: TMVar GHC.Types.Any
>     Prelude Control.Concurrent.STM>
>
> I would think `var1 :: TMVar a` as the documentation says it should.
> Reading on `GHC.Types` `Any` seems to be a type family related to some
> laws on `unsafeCoerce`. Can anybody explain me why is this sensible
> defaulting and how to obtain the expected result?

There's a fine distinction here: The docs don't specify:

`var1 :: forall a. TMVar a`

but rather:

    `newEmptyTMVar :: forall a.  STM (TMVar a)`.

I've inserted the explicit foralls for clarity.

Suppose the behavior was as you expected (I'll use regular MVars just
for brevity):

    var <- newEmptyMVar
    ghci> :t var
    var :: forall a. MVar a

Then, because the variable is polymorphic, we should be able to do:

    putMVar var "Hello"

and, we should also be able to do:

    putMVar var 43

But this is clearly unsafe, because we've put values of two different
types in the same MVar!

In a full program, what would most likely happen is, the first time GHC
sees a use of putMVar, it constrains the type variable to match that
type. In something like this:


    do
        var <- newEmptyMVar
        putMVar var "hello"
        ...

On the second line, GHC constrains the `a` type variable to be `String`,
and so marks that particular use of `newEmptyMVar` as having been used
at type `IO (MVar String)`.

If we don't actually do anything with the MVar, like:

    someAction = do
        var <- newEmptyMVar
        ...
        return var

then `someAction` is inferred to be of type `forall a. IO (MVar a)`,
just like `newEmptyMVar` itself. The constraining will happen wherever
the MVar actually ends up getting used.

But, in the REPL, we're in this weird state where we have access to the
variable and can as what it's type is, but then things can happen
*later* that will force GHC to change the answer.

-Ian
_______________________________________________
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: Weird defaulting on newEmptyTMVar

Viktor Dukhovni
In reply to this post by Viktor Dukhovni
> On Feb 10, 2019, at 5:07 AM, Viktor Dukhovni <[hidden email]> wrote:
>
> The issues become a bit more clear if we replace the "<-" with
> unsafePerformIO:
>
>    ...> :m + System.IO.Unsafe
>    ...> let v = unsafePerformIO newEmptyMVar
>    ...> :t v
>    v :: MVar a
>    ...> putMVar v (1 :: Int)
>    ...> let x = unsafePerformIO (readMVar v)
>    ...> :t x
>    x :: a

Taking it further, one quickly runs into real trouble:

  --- foo.hs
  {-# LANGUAGE TypeApplications #-}
  module Main (main) where

  import Control.Concurrent.MVar
  import System.IO.Unsafe

  main :: IO ()
  main = do
    let v = unsafePerformIO newEmptyMVar
    putMVar v (42 :: Int)
    let x = unsafePerformIO (readMVar v)
    print $ x + 0             -- OK
    print $ x + 3.0           -- Weird
    print $ "oops" ++ x       -- Bad
    readMVar @Int x >>= print -- A bridge too far
  ---

  $ ghc foo.hs
  [1 of 1] Compiling Main             ( foo.hs, foo.o )
  Linking foo ...
  $ ./foo
  42
  3.0
  "oops"
  Segmentation fault (core dumped)

So it is interesting to note that "unsafePerformIO" combined with
polymorphic MVars, is sufficient to completely escape not only
protection from race conditions, but also all type safety.
Unsafe code that manages to create, not an "MVar GHC.Types.Any",
but rather an "MVar a", opens a Pandora's box of trouble.

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