Difference between revisions of "Trash/DDC/ClosureTyping"
(Fix typo, improve description of closure names, thanks to bjpope) |
(Remove old stuff on closure masking) |
||
| Line 54: | Line 54: | ||
This type says that <hask>f_unit</hask> is a function that takes a unit value and returns an <hask>Int</hask>, but the <hask>Int</hask> is free in its closure so is shared by all calls to it. The type system does not generalize regions which are free in these closures. |
This type says that <hask>f_unit</hask> is a function that takes a unit value and returns an <hask>Int</hask>, but the <hask>Int</hask> is free in its closure so is shared by all calls to it. The type system does not generalize regions which are free in these closures. |
||
| − | |||
| − | == Closure masking == |
||
| − | Because Disciple has type elaboration there is usually no need to write closures manually. However, in the rare cases you might want to - maybe you're trying to import a foreign function that does something wierd which the regular FFI elaboration doesn't handle - closure masking can help (a little). |
||
| − | |||
| − | For example: |
||
| − | <haskell> |
||
| − | addFour :: forall %r1 %r2 %r3 %r4 %r5 |
||
| − | . Int %r1 -> Int %r2 -($c1)> Int %r3 -($c2)> Int %r4 -($c3 !e1)> Int %r5 |
||
| − | :- !e1 = !{ Read %r1; Read %r2; !Read %r3; !Read %r4 } |
||
| − | , $c3 = ${ a : Int %r1; b : Int %r2; c : Int %r3; } |
||
| − | , $c2 = ${ a : Int %r1; b : Int %r2; } |
||
| − | , $c1 = ${ a : Int %r1; } |
||
| − | |||
| − | </haskell> |
||
| − | |||
| − | Starting from the right-most closure, each successive closure is simply the previous closure without the current argument. |
||
| − | |||
| − | A slightly nicer way of writing this is: |
||
| − | <haskell> |
||
| − | addFour :: forall %r1 %r2 %r3 %r4 %r5 |
||
| − | . Int %r1 -> Int %r2 -($c1)> Int %r3 -($c2)> Int %r4 -($c3)> Int %r5 |
||
| − | :- !e1 = !{ Read %r1; Read %r2; !Read %r3; !Read %r4 } |
||
| − | , $c3 = ${ a : Int %r1; b : Int %r2; c : Int %r3 } |
||
| − | , $c2 = $c3 \ c |
||
| − | , $c1 = $c2 \ b |
||
| − | </haskell> |
||
| − | |||
| − | In this version we use <hask>$c3 \ c</hask> to mean the closure <hask>$c3</hask> ''without'' the regions from the object we've named <hask>c</hask>. |
||
Revision as of 23:21, 24 June 2009
Region sharing
Consider the following function:
f ()
= do x = 5
g () = x
g
Without closure information this function would have the following type:
f :: forall %r. () -> () -> Int %r
Remember that the forall %r at the front of the type is supposed to indicate that the return value is freshly allocated. This is certainly true if we apply both arguments:
twoSeparateInts :: Tuple2 %r1 (Int %r2, Int %r3)
twoSeparateInts = (f () (), f () ())
In twoSeparateInts there are different regions annotation on each of the Int constructors, which means they do not alias, and its safe to treat one as Const and the other as Mutable.
But what happens if we partially apply f? The standard type system will re-generalize the type for the new binding and we're left with:
f_unit :: forall %r1. () -> Int %r1
f_unit = f ()
We've now got a function which returns the same Int every time we call it, but the type says it's supposed to be fresh! The problem here is that x was free in our original definition of g so is shared between applications of it.
Closure typing for region sharing
Closure typing is used to track the sharing of regions between function calls like this one.
The type inferred for f is actually:
f :: forall %r0
. () -> () -($c0)> Int %r0
:- $c0 = x : %r0
The $c0 annotation tells us that this function has a object free in its closure, and that the object contains region %r0. The x : %r0 syntax gives a name to this term, and is pronounced "x of region zero".
Similarly to variables in the expression language, the exact names given to closure terms is not significant to the type system. However, to make inferred types easier to read, DDC names the closure terms in a function's type after the free variables that gave rise to those terms. The user is free to use whatever names they wish in type signatures. Two closure terms with different names but identical right hand sides are taken as being equivalent.
If we use this new type and apply the first argument we have:
f_unit :: () -($c0)> Int %r0
:- $c0 = x : %r0
This type says that f_unit is a function that takes a unit value and returns an Int, but the Int is free in its closure so is shared by all calls to it. The type system does not generalize regions which are free in these closures.