Language.CPS

• http://okmij.org/ftp/tagless-final/course/course.html#CPS

We demonstrate ordinary and administrative-redex--less call-by-value Continuation Passing Style (CPS) transformation that assuredly produces well-typed terms and is patently total.

Our goal here is not to evaluate, view or serialize a tagless-final term, but to transform it to another one. The result is a tagless-final term, which we can interpret in multiple ways: evaluate, view, or transform again. We first came across transformations of tagless-final terms when we discussed pushing the negation down in the simple, unityped language of addition and negation. The general case is more complex. It is natural to require the result of transforming a well-typed term be well-typed. In the tagless-final approach that requirement is satisfied automatically: after all, only well-typed terms are expressible. We require instead that a tagless-final transformation be total. In particular, the fact that the transformation handles all possible cases of the source terms must be patently, syntactically clear. The complete coverage must be so clear that the metalanguage compiler should be able to see that, without the aid of extra tools.

Since the only thing we can do with tagless-final terms is to interpret them, the CPS transformer is written in the form of an interpreter. It interprets source terms yielding transformed terms, which can be interpreted in many ways. In particular, the terms can be interpreted by the CPS transformer again, yielding 2-CPS terms. CPS transformers are composable, as expected.

A particular complication of the CPS transform is that the type of the result is different from the type of the source term: the CPS transform translates not only terms but also types. Moreover, the CPS type transform and the arrow type constructor do not commute. For that reason, we have to introduce an extended Symantics class, ESymantics, which makes the meaning of function types dependent on a particular interpreter. As it turns out, we do not have to re-write the existing Symantics terms: we can re-interpret any old terms in the extended Symantics. Conversely, any extended Symantics term can be interpreted using any old, legacy, Symantics interpreter. The CPS transform is an extended Symantics interpreter proper.

The ordinary (Fischer or Plotkin) CPS transform introduces many administrative redices, which make the result too hard to read. Danvy and Filinski proposed a one-pass CPS transform, which relies on the metalanguage to get rid of the administrative redices. The one-pass CPS transform can be regarded as an example of the normalization-by-evaluation.

Extending Symantics:

Parameterizing the arrows by the interpreter

CBAny.hs: type Arr exp a b = exp a -> exp b

Emulating ML modules in Haskell

How to interpret arrows and other types

type family Arr repr a b :: *

class ESymantics repr where

Methods

int :: Int -> repr Int

add :: repr Int -> repr Int -> repr Int

lam :: (repr a -> repr b) -> repr (Arr repr a b)

app :: repr (Arr repr a b) -> repr a -> repr b

Instances

Symantics repr => ESymantics (Lg repr)

ESymantics repr => ESymantics (CPS1 repr w)

ESymantics repr => ESymantics (CPS repr w)

Like Symantics in CBAny.hs

All old Symantics terms can be re-interpreted in the

extended Symantics

type family GenArr repr a :: *

newtype ExtSym repr a

Constructors

ExtSym

Fields

unExtSym :: repr (GenArr repr a)

Instances

ESymantics repr => Symantics (ExtSym repr)

The converse: ESymantics => Symantics

Inject _all_ old interpreters into the new one

newtype Lg repr a

Constructors

Lg

Fields

unLg :: repr a

Instances

Symantics repr => ESymantics (Lg repr)

legacy :: Symantics repr => (repr a -> b) -> Lg repr a -> b

We can use all existing interpreters _as they are_

CBV CPS transform

CPS[ value ] = k -> k $ CPSV[ value ]

CPS[ e1 e2 ] =

k ->

CPS[ e1 ] (v1 ->

CPS[ e2 ] (v2 ->

v1 v2 k))

(similar for addition)

CPSV[ basec ] = basec

CPSV[ x ] = x

CPSV[ x.e ] = x -> CPS[ e ]

Danvy: CPS is *the* canonical transform

CPS on types is NOT the identity

newtype CPS repr w a

Constructors

CPS

Fields

cpsr :: repr (Arr repr (Arr repr a w) w)

Instances

ESymantics repr => ESymantics (CPS repr w)

cpsk :: ESymantics repr => (repr (Arr repr a w) -> repr w) -> CPS repr w a

appk :: ESymantics repr => CPS repr w a -> (repr a -> repr w) -> repr w

CPS of a value

cpsv :: ESymantics repr => repr a -> CPS repr w a

Applying the transform, evaluate afterwards

The case of administrative redices

Composing interpreters: doing CPS twice

One-pass CPS transform

newtype CPS1 repr w a

Constructors

CPS1

Fields

cps1r :: (repr a -> repr w) -> repr w

Instances

ESymantics repr => ESymantics (CPS1 repr w)

reflect :: ESymantics repr => ((repr a -> repr w) -> repr w) -> repr (Arr repr (Arr repr a w) w)

reflect e = lam (e . app)

CPS1 of a value

cps1v :: ESymantics repr => repr a -> CPS1 repr w a

Applying the transform, evaluate afterwards

The result is indeed much nicer

Composing interpreters: doing CPS twice

Lessons

The output of CPS is assuredly typed

The conversion is patently total

Composable transformers in the tagless final style