- 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
- Like Symantics in CBAny.hs
- All old Symantics terms can be re-interpreted in the
- extended Symantics
- The converse: ESymantics => Symantics
- Inject _all_ old interpreters into the new one
- 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
- CPS of a value
- Applying the transform, evaluate afterwards
- The case of administrative redices
- Composing interpreters: doing CPS twice
- One-pass CPS transform
- reflect e = lam (e . app)
- CPS1 of a value
- 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

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.

- type family Arr repr a b :: *
- class ESymantics repr where
- type family GenArr repr a :: *
- newtype ExtSym repr a = ExtSym {}
- newtype Lg repr a = Lg {
- unLg :: repr a

- legacy :: Symantics repr => (repr a -> b) -> Lg repr a -> b
- newtype CPS repr w a = CPS {}
- 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
- cpsv :: ESymantics repr => repr a -> CPS repr w a
- newtype CPS1 repr w a = CPS1 {
- cps1r :: (repr a -> repr w) -> repr w

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

# 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

class ESymantics repr whereSource

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

ESymantics repr => Symantics (ExtSym repr) |

# The converse: ESymantics => Symantics

# Inject _all_ old interpreters into the new one

# 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

ESymantics repr => ESymantics (CPS repr w) |

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

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

# CPS of a value

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

# Applying the transform, evaluate afterwards

# The case of administrative redices

# Composing interpreters: doing CPS twice

# One-pass CPS transform

ESymantics repr => ESymantics (CPS1 repr w) |

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

# reflect e = lam (e . app)

# CPS1 of a value

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