{-# 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."

## No comments:

Post a Comment