Skip to content

Add roles declarations to allow safe coercions #16

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Nov 18, 2020
Merged

Add roles declarations to allow safe coercions #16

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions src/Foreign/Object.purs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,8 @@ import Unsafe.Coerce (unsafeCoerce)
-- | `Object a` represents a homogeneous JS Object with values of type `a`.
foreign import data Object :: Type -> Type

type role Object representational

foreign import _copyST :: forall a b r. a -> ST r b

-- | Convert an immutable Object into a mutable Object
Expand Down
2 changes: 2 additions & 0 deletions src/Foreign/Object/ST.purs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,8 @@ import Data.Maybe (Maybe(..))
-- | that of `Object a`, except that mutation is allowed.
foreign import data STObject :: Region -> Type -> Type

type role STObject nominal representational

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I know you've been doing nominal in situations like this, but shouldn't this be phantom? At the end of the day, Region is a skolem type, so it shouldn't matter what type it gets coerced to, correct?

Also, I'm fine with leaving this as nominal and changing it to phantom in a later release.

Copy link
Contributor

@hdgarrood hdgarrood Nov 17, 2020 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't see how you get from Region being a skolem type to it not mattering what it gets coerced to, that line of argument doesn't make sense to me. I think nominal is correct here: I think it's possible that if this were phantom then you could coerce an STObject in a way that allows the mutable reference to escape its scope. At least, we would need to prove that this wouldn't be an issue before being able to justify any role other than nominal here.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don’t understand what could go wrong if we could coerce between two arbitrary regions, until then I would be reluctant to relax the role. That’s also consistent with Haskell:

module Example where

import GHC.ST (ST)
import Data.Coerce (coerce)

newtype N a = N a

example :: ST s0 a -> ST s1 (N a)
example = coerce
Example.hs:9:11: error:
    • Couldn't match type ‘s0’ with ‘s1’ arising from a use of ‘coerce’
      ‘s0’ is a rigid type variable bound by
        the type signature for:
          example :: forall s0 a s1. ST s0 a -> ST s1 (N a)
        at Example.hs:8:1-33
      ‘s1’ is a rigid type variable bound by
        the type signature for:
          example :: forall s0 a s1. ST s0 a -> ST s1 (N a)
        at Example.hs:8:1-33
    • In the expression: coerce
      In an equation for ‘example’: example = coerce
    • Relevant bindings include
        example :: ST s0 a -> ST s1 (N a) (bound at Example.hs:9:1)
  |
9 | example = coerce
  |           ^^^^^^

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here's an example showing why ST ref types need to have nominal roles for their region parameters:

module Main where

import Prelude
import Effect (Effect)
import Control.Monad.ST (ST)
import Control.Monad.ST as ST
import Control.Monad.ST.Ref (STRef)
import Control.Monad.ST.Ref as STRef
import Effect.Console as Console
import Safe.Coerce

globalRef :: forall r. STRef r Int
globalRef = ST.run do
  r <- STRef.new 0
  pure (coerce r)

next :: Unit -> Int
next _ = ST.run do
  r <- STRef.read globalRef
  _ <- STRef.write (r + 1) globalRef
  pure (r + 1)

main :: Effect Unit
main = do
  Console.log (show (next unit))
  Console.log (show (next unit))
  Console.log (show (next unit))

which produces the output

1
2
3

showing that the next function is not pure.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh right, the regions r1 and r2 in Control.Monad.ST.Ref.new :: forall a r1 r2. a -> ST r1 (STRef r2 a) have to be the same or the ref can escape its mutable scope. Thanks a lot! That’s quite clear now.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah... Well, that settles that! Nice example @hdgarrood!

-- | Create a new, empty mutable object
foreign import new :: forall a r. ST r (STObject r a)

Expand Down