{-# LANGUAGE NoMonomorphismRestriction #-} -- Deriving type-safe printf in direct-style, using -- shift/reset with effectful typing (supporting the answer-type -- modification and polymorphism) module Derive5 where import Control.Monad import ShiftResetGenuine -- Constructors and deconstructors of a particular sequence -- See the end of derive5.ml nilA :: Monadish m => a -> m s s a nilA = ret {- consA :: (Monadish m) => h -> (sigma -> m a b tau) -> (h -> m b g sigma) -> m a g tau -} consA h t = \f -> f h >== \x -> t x un_consA x = reset (x (\h -> shift (\t -> ret (h,t)))) -- The example of the de-construction: l0 = consA 'a' nilA l0r = fst \$ run \$ un_consA l0 -- 'a' l1 = consA 5 (consA 'a' (consA 'f' nilA)) (h1,l11) = run \$ un_consA l1 -- h1 is 5 (h2,l12) = run \$ un_consA l11 -- h2 is 'a' nilS :: String nilS = "" consS :: String -> String -> String consS = (++) -- litP4 :: (Monadish m) => String -> (t -> m a g String) -> t -> m a g String litP4 str = \tD arg -> tD arg >== ret . consS str intP4 = \tD arg -> un_consA arg >== \(n,l2) -> tD l2 >== ret . consS (show (n::Int)) charP4 = \tD arg -> un_consA arg >== \(c,l2) -> tD l2 >== ret . consS (show (c::Char)) nilDP = \x -> x nilS consDP d acc = \x -> d acc x desc0 = consDP (litP4 "lit") \$ consDP intP4 nilDP desc0r = run \$ desc0 (consA 1 nilA) -- "lit1" descP4 = consDP intP4 (consDP (litP4 "-th character after ") (consDP charP4 (consDP (litP4 " is ") (consDP charP4 nilDP)))) descr4 = run \$ descP4 (consA 5 (consA 'a' (consA 'f' nilA))) -- "5-th character after 'a' is 'f'" t0 = \h -> reset (shift (\k -> desc0 k) >== \f -> f h) {- We would like the argument sequence to be just the application of the arguments. We would like to transform (xxx x1 x2 x3) to (fun f -> f x1 x2 x3), which is needed as an argument to descP4. We can do that if we enclose the whole printf expression in reset. -} -- Apply a monadish f to the pure argument x app fm x = fm >== \f -> f x t1 = (shift descP4) `app` 5 `app` 'a' `app` 'f' -- t1 :: C String String String t1r = run \$ reset t1 -- "5-th character after 'a' is 'f'" -- A different take, viewing un_consA as `reading' from a sequence is_nilA1 _ = () un_consA1 arg = shift (\k -> ret \$ \y -> k (y,arg)) litP5 = litP4 -- Inline un_consA1 into intP4 intP5 = \tD arg -> shift (\k -> ret \$ \y -> k (y,arg)) >== \(n,arg) -> tD arg >== ret . consS (show (n::Int)) charP5 = \tD arg -> un_consA1 arg >== \(c,l2) -> tD l2 >== ret . consS (show (c::Char)) nilDP5 _ = ret nilS desc05 = consDP (litP5 "lit") \$ consDP intP5 nilDP5 desc05r = run \$ (reset (desc05 ()) `app` 5) -- "lit5" descP5 = consDP intP5 (consDP (litP5 "-th character after ") (consDP charP5 (consDP (litP5 " is ") (consDP charP5 nilDP5)))) printf5 desc = reset (desc ()) descr5 = run \$ printf5 descP5 `app` 5 `app` 'a' `app` 'f' -- "5-th character after 'a' is 'f'" -- After several transformations described in the paper (eta-reductions mainly) intP6 = \tD () -> shift (\k -> ret k) >== \n -> tD () >== ret . consS (show (n::Int)) litP7 str = \() -> ret str intP7 = \() -> shift (\k -> ret k) >== \n -> ret (show (n::Int)) charP7 = \() -> shift (\k -> ret k) >== \c -> ret (show (c::Char)) infixr 7 ^^^ -- Lifted string concatenation f ^^^ g = \() -> f () >== \s1 -> g () >== \s2 -> ret (s1 ++ s2) printf7 desc = reset \$ desc () descP7 = intP7 ^^^ (litP7 "-th character after ") ^^^ charP7 ^^^ (litP7 " is ") ^^^ charP7 descr7 = run \$ printf7 descP7 `app` 5 `app` 'a' `app` 'f' -- "5-th character after 'a' is 'f'"