[http://trac.haskell.org/ddc/wiki/Language/Overview < Overview]

= Polymoprhic Update =

== 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

 	putStrLn $ show $ fst getSet ()   -- prints '5'

	snd getSet 23         -- update the box
	putStrLn $ show $ 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"]

       putStrLn $ show $ 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 extended 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 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 closure of a function.