[Haskell-cafe] Running classical logic
haskell-cafe at jbapple.com
Fri Mar 28 02:00:57 EDT 2008
We can't safely extract a t out of IO t, but we can run an IO t,
interact with the environment, and then see the t.
Griffin ( http://citeseer.ist.psu.edu/griffin90formulaeastypes.html )
explained that we can do the same thing with (t -> r) -> r by
interacting with the context. That is, he defined a function
c :: ((t -> r) -> r) -> t
buy interaction with the reduction context of calls to c.
I don't expect such a function to be definable in Haskell without some
magic, but even with magic, I'm not sure how to write such a function.
On #haskell a couple of days ago, we came up with
data Empty deriving Typeable
toEmpty :: a -> Empty
toEmpty = unsafeCoerce
fromEmpty :: Empty -> a
fromEmpty = unsafeCoerce
type Bot = forall x . x
griffinC :: Cont Bot a -> IO a
griffinC (Cont f) =
key <- newUnique
(evaluate $ f $ \v -> throwDyn (hashUnique key,toEmpty v))
(\x -> case x of
DynException d ->
case fromDynamic d of
Just (u,y) -> if u == hashUnique key
then return $ fromEmpty y
else throwIO x
Nothing -> throwIO x
_ -> throwIO x)
The Unique is used to keep the later griffinC calls from being cast to
the wrong types.
The more I look at this, the less I understand it.
P.S. Thanks to #haskell, and especially roconnor for the fine help
More information about the Haskell-Cafe