- 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