[Haskell-cafe] Running classical logic

28 Mar 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) =
    do
      key <- newUnique
      catch
        (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.

Any clues?

Jim

P.S. Thanks to #haskell, and especially roconnor for the fine help

[Haskell-cafe] Running classical logic

Jim Apple