reflecting and reifying the state monad

The Haskell code below was inspired by Andrej Bauer's visit last week, as well as thinking more about this, this, and this since writing this.

---

{-# LANGUAGE RankNTypes, FlexibleInstances #-}

-- A "negative type" is a datatype of continuations, indexed by answer
-- type.  Given such a description, we can define values, "algebras",
-- and "handlers" as control expressions ("double negations") with
-- different answer type constraints
-- (cf. http://polaro.blogspot.com/2010/05/five-kinds-of-double-negation.html)

newtype Value neg = Val { runVal :: forall r. neg r -> r }
newtype Algebra neg r = Alg { runAlg :: neg r -> r }
newtype Handler neg r1 r2 = Han { runHandle :: neg r1 -> r2 }

infixr 0 `plugV`, `plugA`, `plugH`

plugV :: neg r -> Value neg -> r
k `plugV` v = runVal v k

plugA :: neg r -> Algebra neg r -> r
k `plugA` v = runAlg v k

plugH :: neg r -> Handler neg r r' -> r'
k `plugH` v = runHandle v k

-- We define the negative type Cell s

data Cell s r = Update s (Cell s r)
              | Lookup (s -> Cell s r)
              | Return r

-- Example: given an initial state, we can create a cell value...

new :: s -> Value (Cell s)
new s = Val newVal
    where
      newVal (Update s' k) = k `plugV` new s'
      newVal (Lookup ks) = ks s `plugV` new s
      newVal (Return a) = a

-- Example: perform some operations on an initial state...

r1 = (Lookup $ \s ->
      Update (s-1) $
      Lookup $ \s' ->
      Return (s'+1))
     `plugV`
     new 2
-- r1 = 2

-- Monadic reification and reflection

reify :: Cell s a -> s -> (s,a)
reify k s = k `plugH` Han reifyHandle
    where
      reifyHandle (Update s' k') = reify k' s'
      reifyHandle (Lookup ks) = reify (ks s) s
      reifyHandle (Return a) = (s,a)

reflect :: (s -> (s,a)) -> Cell s a
reflect m = Lookup $ \s ->
            let (s',a) = m s in
            Update s' $
            Return a

-- Example: Normalization by reification and reflection

prog1 = Update 0 $
        Lookup $ \s ->
        Return (s + 1)
prog2 = Lookup $ \s ->
        Update 2 $
        Update 0 $
        Return 1

-- a bit of code for printing cell continuations (prints only a small
-- segment of lookup tables)
instance Show r => Show (Cell Integer r) where
    show (Update s k) = "upd " ++ show s ++ "; " ++ show k
    show (Lookup ks) = show (map (\s -> (s, ks s)) [0..3])
    show (Return a) = "ret " ++ show a

-- *Main> prog1
-- upd 0; [(0,ret 1),(1,ret 2),(2,ret 3),(3,ret 4)]
-- *Main> prog2
-- [(0,upd 2; upd 0; ret 1),(1,upd 2; upd 0; ret 1),(2,upd 2; upd 0; ret 1),(3,upd 2; upd 0; ret 1)]
-- *Main> reflect(reify prog1)
-- [(0,upd 0; ret 1),(1,upd 0; ret 1),(2,upd 0; ret 1),(3,upd 0; ret 1)]
-- *Main> reflect(reify prog2)
-- [(0,upd 0; ret 1),(1,upd 0; ret 1),(2,upd 0; ret 1),(3,upd 0; ret 1)]

---

Otherwise, things have been good. This blog has been quiet for a while, but I'm still learning a lot from amazing people. Though I can't resist quoting Henry Miller: "It is now the fall of my second year in Paris. I was sent here for a reason I have not yet been able to fathom."