Version franaise
Home About Download Resources Contact us

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
A Monadic Framework for Subcontinuations
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2005-10-17 (06:34)
From: Paul Snively <psnively@m...>
Subject: A Monadic Framework for Subcontinuations

I'm trying to work through < 
simonpj/papers/control/control.pdf>, which is to say that I'm  
attempting to transliterate some interesting Haskell code to O'Caml.  
On page 23, we find the following "refined interface:"

--------------------------snip snip--------------------------
data CC r a                                        -- Abstract
data Prompt r a                                 -- Abstract
data SubCont r a b                           -- Abstract

instance Monad (CC r)

runCC :: (∀ r⋅ CC r a) ➝ a
newPrompt :: CC r (Prompt r a)
pushPrompt :: Prompt r a ➝ CC r a ➝ CC r a
withSubCont :: Prompt r b ➝ (SubCont r a b ➝ CC r b) ➝ CC r a
pushSubCont :: SubCont r a b ➝ CC r a ➝ CC r b
--------------------------snip snip--------------------------

I haven't read a lot of Haskell interfaces, to put it mildly. The  
text makes it seem that "r" here is a phantom type. I'm not sure how  
to interpret the universal quantification, assuming that I'm right  
about r being a phantom type. I'm only beginning to try to use  
phantom types anyway. So surely the following can't be correct:

--------------------------snip snip--------------------------
module type Continuation =
   type ('r, 'a) cc
   type ('r, 'a) prompt
   type ('r, 'a, 'b) subcont

   val runCC : ('r, 'a) cc -> 'a
   val newPrompt : ('r, ('r, 'a) prompt) cc
   val pushPrompt : ('r, 'a) prompt -> ('r, 'a) cc -> ('r, 'a) cc
   val withSubCont : ('r, 'b) prompt -> (('r, 'a, 'b) subcont -> ('r,  
'b) cc) ->('r, 'a) cc
   val pushSubCont : ('r, 'a, 'b) subcont -> ('r, 'a) cc -> ('r, 'b) cc
--------------------------snip snip--------------------------

Am I right about r being a Phantom Type? What does the universal  
quantification imply in this context? Can I get away with this  
"blowing it off" that I've done above? I'll worry about the actual  
implementation in a bit. Right now, I just wonder if I'm not  
misunderstanding something in the interface.

Many thanks and best regards,