Version 3 (modified by benl, 9 years ago) (diff) |
---|
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 (outer most) closure of a function.