Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

STRef and phantom types

Tags:

haskell

Does s in STRef s a get instantiated with a concrete type? One could easily imagine some code where STRef is used in a context where the a takes on Int. But there doesn't seem to be anything for the type inference to give s a concrete type.

Imagine something in pseudo Java like MyList<S, A>. Even if S never appeared in the implementation of MyList instantiating a concrete type like MyList<S, Integer> where a concrete type is not used in place of S would not make sense. So how can STRef s a work?

like image 321
user782220 Avatar asked Oct 08 '14 04:10

user782220


2 Answers

tl;dr - in practice it seems it always gets initialised to RealWorld in the end

The source notes that s can be instantiated to RealWorld inside invocations of stToIO, but is otherwise uninstantiated:

-- The s parameter is either

-- an uninstantiated type variable (inside invocations of 'runST'), or

-- 'RealWorld' (inside invocations of 'Control.Monad.ST.stToIO').

Looking at the actual code for ST however it seems runST uses a specific value realWorld#:

newtype ST s a = ST (STRep s a)
type STRep s a = State# s -> (# State# s, a #)

runST :: (forall s. ST s a) -> a
runST st = runSTRep (case st of { ST st_rep -> st_rep })

runSTRep :: (forall s. STRep s a) -> a
runSTRep st_rep = case st_rep realWorld# of
                        (# _, r #) -> r

realWorld# is defined as a magic primitive inside the GHC source code:

realWorldName     = mkWiredInIdName gHC_PRIM  (fsLit "realWorld#")
                                    realWorldPrimIdKey realWorldPrimId

realWorldPrimId :: Id   -- :: State# RealWorld
realWorldPrimId = pcMiscPrelId realWorldName realWorldStatePrimTy
                     (noCafIdInfo `setUnfoldingInfo` evaldUnfolding
                                  `setOneShotInfo` stateHackOneShot)

You can also confirm this in ghci:

Prelude> :set -XMagicHash
Prelude> :m +GHC.Prim
Prelude GHC.Prim> :t realWorld#
realWorld# :: State# RealWorld
like image 144
GS - Apologise to Monica Avatar answered Oct 25 '22 08:10

GS - Apologise to Monica


From your question I can not see if you understand why the phantom s type is there at all. Even if you did not ask for this explicitly, let me elaborate on that.

The role of the phantom type

The main use of the phantom type is to constrain references (aka pointers) to stay "inside" the ST monad. Roughly, the dynamically allocated data must end its life when runST returns.

To see the issue, let's pretend that the type of runST were

runST :: ST s a -> a

Then, consider this:

data Dummy
let var :: STRef Dummy Int
    var    = runST (newSTRef 0)
    change :: () -> ()
    change = runST (modifySTRef var succ)
    access :: () -> Int
    result :: (Int, ())
    result = (access() , change())
 in result

(Above I added a few useless () arguments to make it similar to imperative code)

Now what should be the result of the code above? It could be either (0,()) or (1,()) depending on the evaluation order. This is a big no-no in the pure Haskell world.

The issue here is that var is a reference which "escaped" from its runST. When you escape the ST monad, you are no longer forced to use the monad operator >>= (or equivalently, the do notation to sequentialize the order of side effects. If references are still around, then we can still have side effects around when there should be none.

To avoid the issue, we restrict runST to work on ST s a where a does not depend on s. Why this? Because newSTRef returns a STRef s a, a reference to a tagged with the phantom type s, hence the return type depends on s and can not be extracted from the ST monad through runST.

Technically, this restriction is done by using a rank-2 type:

runST :: (forall s. ST s a) -> a

the "forall" here is used to implement the restriction. The type is saying: choose any a you wish, then provide a value of type ST s a for any s I wish, then I will return an a. Mind that s is chosen by runST, not by the caller, so it could be absolutely anything. So, the type system will accept an application runST action only if action :: forall s. ST s a where s is unconstrained, and a does not involve s (recall that the caller has to choose a before runST chooses s).

It is indeed a slightly hackish trick to implement the independence constraint, but it does work.

On the actual question

To connect this to your actual question: in the implementation of runST, s will be chosen to be any concrete type. Note that, even if s were simply chosen to be Int inside runST it would not matter much, because the type system has already constrained a to be independent from s, hence to be reference-free. As @Ganesh pointed out, RealWorld is the type used by GHC.

You also mentioned Java. One could attempt to play a similar trick in Java as follows: (warning, overly simplified code follows)

interface ST<S,A> { A call(); }
interface STAction<A> { <S> ST<S,A> call(S dummy); }
...
<A> A runST(STAction<A> action} {
    RealWorld dummy = new RealWorld();
    return action.call(dummy).call();
}

Above in STAction parameter A can not depend on S.

like image 25
chi Avatar answered Oct 25 '22 07:10

chi