Version 73 (modified by chak, 7 years ago) (diff)


Closure conversion without classes


The closure type

We represent closures by


and define closure creation and application as

lam f = const f :$ ()



Overview and invariants


  • For each function definition
    f::ty = e
    create a closure-converted function definition for f_cc, defining the closure-converted version of f, and a definition for f with its original type, that defines it in terms of f_cc:
    f_cc::ty^ = e^
    f::ty = fr iso<ty> f_cc
    where ty^ is the closure-converted version of ty, and e^ is the closure-converted version of e.
  • For each data type T, create a closure-converted data type T_CC, whose constructors use (:->) instead of (->).
  • The value iso<ty> is a pair of functions, converting to and fro between ty and ty^. Like "^", the iso<ty> thing should be considered as a meta-function that works recursively on ty.


  e :: ty     implies       e^ :: ty^

  to iso<ty> :: ty -> ty^
  fr iso<ty> :: ty^ -> ty


Conversion status




  3. A converted variant T_CC exists and differs from T.



Converting types

Conversion of type terms

We determine the converted type t^ of t as follows:

T^            = T_CC , if T_CC exists
              = T    , otherwise
a^            = a_CC
                             or kindOf t2 == #
              = t1^ :-> t2^, otherwise
(t1 t2)^      = t1^ t2^
(forall a.t)^ = forall a_CC.t^

Here some examples,



Conversion constructors


Conversion pairs




Types of convercion constructors



where type conversion t^ is defined below.

As an example, consider


The type of the conversion constructor is as follows :

  forall f f_CC. 
    (forall a a_CC. 
    T f :<->: T_CC f_CC

The conversion constructor might be implemented as

isoT isof = toT :<->: frT


Moreover, the conversion constructor for function arrows is





iso<T>          = isoT           , if T_CC exists
                = idIso<*>       , otherwise
iso<a::k>       = idIso<k>
                                   or kindOf t2 == #
                = isoArr         , otherwise 
                    iso<t1> iso<t2>


idIso<*>      = id :<->: id



would work, but it doesn't always. Take this example

data T a = MkT a
unit :: T a -> a
unit (MkT x) = x

-- converted
foo t u = u t 1

-- not converted
bar = foo unit



Here some example conversions:

iso<Int -> Int>     = isoArr isoInt isoInt
                                      (id :<->: id))

Converting type declarations

Conversion rules



Moreover, we handle other forms of type constructors as follows:


Conversion constructor


Converting data constructors


MkT :: (Int -> Int) -> Int

the converted worker is





For example, when we convert

data Int = I# Int#

we get Int_CC = Int and we have

isoInt :: Int :<->: Int
isoInt = toInt :<->: frInt
    toInt (I# i#) = I# i#
    frInt (I# i#) = I# i#

As another example,

data Maybe a = Nothing | Just a

implies Maybe_CC = Maybe and

isoMaybe isoa = toMaybe :<->: frMaybe
    toMaybe isoa Nothing  = Nothing
    frMaybe isoa Nothing  = Nothing

Converting classes and instances


As an example, assume Num Int were defined as

class Num a where
  (+)    :: a -> a -> a
  negate :: a -> a
instance Num Int where
  (+)    = primAddInt
  negate = primNegateInt

with the Core code being

data Num a = 
  Num {
    negate :: a -> a
dNumInt = Num Int
dNumInt = Num primAddInt primNegateInt

Then, closure conversion gives us


dNumInt_CC :: Num_CC Int   -- as Int_CC = Int
dNumInt_CC = Num_CC 
               (to isoIntToIntToInt primAddInt) 
               (to isoIntToInt primNegateInt)
    isoIntToIntToInt = isoArr isoInt isoIntToInt
    isoIntToInt      = isoArr isoInt isoInt

Converting value bindings


For every binding

f :: t = e

we generate

f_CC :: t^ = e^



f :: t = fr iso<t> f_CC



add :: Num a -> a -> a

we generate

add :: Num a -> a -> a
add = fr isoFun add_CC
             (id :<->: id)        `isoArr`
             (id :<->: id)

add_CC = lam $ \dNum -> 


Converting terms

To keep the translation rules simpler, we assume that for every converted data constructor C_CC :: forall t1 -> .. -> tm -> t, there is a conversion wrapper

$WC_CC :: forall t1 :-> .. :-> tm :-> t
$WC_CC = /\ -> lam_m (C_CC@a1@..@an)

where the family of functions

lam_1 :: (a1 -> b) -> (a1 :-> b)
lam_1 = lam

lam_n :: (a1  -> ..  -> an  -> b)
      -> (a1 :-> .. :-> an :-> b)
lam_n f = 
  lam_(n-1) $ 
    \x1 .. x(n-1) -> uncurry_(n-1) f :$ (x1, .., x(n-1)

turns an n-ary function into an n-ary closure. (NB: This is not the same as (to iso<..>) for that type, as we do not convert the types of the arguments of the function.)

We translate terms as follows:

  | if C_CC exists       = $WC_CC
  | if x_CC exists       = x_CC
  | otherwise            = to iso<t> x
cc[[lit]]                = lit
cc[[e@t]]                = cc[[e]]@t^
cc[[\x -> e]]            = (\(y1, .., yn) x_CC -> cc[e]]) :$
                           (y1, .., yn)
    y1 .. yn = FV e
cc[[/\a -> e]]           = /\a -> cc[e]]
cc[let x = e1 in e2]     = let x_CC = cc[[e1]] in cc[[e2]]
cc[[case e x::t of alts]]= case cc[[e]] x_CC::t^
                           of cc[[alts]]
cc[[e `cast` t]]         = cc[[e]] `cast` t^

cc[[alt1; ..; altn]]    = cc[[alt1]]; ..; cc[altn]]
cc[[default -> e]]      = default -> cc[[e]]
cc[[C x1 .. xn -> e]]
  | if C_CC exists      = C_CC x1_CC .. xn_CC -> cc[[e]]
  | otherwise           = C x1 .. xn -> cc[[e]]



