DDC/PolymorphicUpdate

Get/Set

Consider the following function:

makeGetSet :: forall a. a -> (() -> a, a -> ())
makeGetSet x
 = do 	box	= Just x
	get ()	= case box of { Just z -> z; }
	set z	= box#x #= z
	(get, set)

This function allocates a box which can store a value, and returns a tuple of functions to get and set that value.

As the function is polymorphic, we can create boxes of whatever type we would like:

main ()
 = do	getSet :: (() -> Int, Int -> ())
        getSet	= makeGetSet 5

 	out $ fst getSet ()   -- prints '5'

	snd getSet 23         -- update the box
	out $ fst getSet ()   -- prints '23'

The trouble comes when we create a box containing a value of polymorphic type. Without closure typing we could define:

        ...
        getSet2 :: forall a. (() -> [a], [a] -> ())
        getSet2 = makeGetSet []

When a list is empty, we can treat it as being of any type (forall a. [a]), but suppose we update the box containing it at two different types...

       snd getSet2 [23]
       snd getSet2 ["trouble"]

       out $ fst getSet2 ()

The type of getSet2 has forall a. at the front, so there is nothing to stop us from calling the set function at both [Int] and [String], but what should the type be when use the get function in the last line?

Dangerous type variables

Ultimately, the problem illustrated above arose because there wasn't a mechanism to track the sharing of data between successive calls to getSet2. When makeGetSet was evaluated it created a shared mutable object (the box) and then returned functions that had this object free in their closure.

In Disciple, makeGetSet has the full type:

makeGetSet
        :: forall a %r0 %r1
        .  a -> Tuple2 %r1 (() -(!e0 $c0)> a) (a -(!e1 $c1)> ())
        :- !e0        = !Read %r0
        ,  !e1        = !{!Read %r0; !Write %r0}
        ,  $c0        = ${box : %r0; box : %r0 $> a}
        ,  $c1        = ${box : %r0; box : %r0 $> a}
        ,  Base.Mutable %r0

In this type, we see the new closure term (box : %r0 $> a). This term says that the closure contains an object named box which is in a region %r0, and the type of the object includes a variable 'a'. When %r0 is Mutable we say that a is dangerous, and dangerous variables are never generalised when they are free in the (outer most) closure of a function.