Browse thread
A Monadic Framework for Subcontinuations
- Paul Snively
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
| Date: | -- (:) |
| From: | Paul Snively <psnively@m...> |
| Subject: | A Monadic Framework for Subcontinuations |
O'Camlers,
I'm trying to work through <http://research.microsoft.com/users/
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 =
sig
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
end
--------------------------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,
Paul