{-# LANGUAGE RebindableSyntax, NoMonomorphismRestriction #-} -- A simple EDSL with answer-type modifying shift/reset -- emulate direct-style shift-reset. We can implement the examples -- from Kenichi Asai's tutorial like list append that do require -- answer-type modification. -- We rely RebindableSyntax to make the Haskell code look like -- OChaCaml code. It is up to the reader to determine how well -- we succeeded. -- This code is the veneer over ShiftResetGenuine, which is -- an implementation of the calculus lambda-sr-let -- Polymorphic delimited continuations -- Asai and Kameyama, APLAS 2007 -- http://logic.cs.tsukuba.ac.jp/~kam/paper/aplas07.pdf -- hereafter, AK07 -- We try to hide the Monadish plumbing. module SRTest where import ShiftResetGenuine import Prelude (Int, Show(..), (.)) import qualified Prelude -- ------------------------------------------------------------------------ -- The examples -- OchaCaml: -- let f x = reset (fun () -> 3 + shift (fun k -> k) - 1) x ;; f = reset (3 + shift (\k -> return k) - 1) -- pure function application tf = run (f \$: 10) -- 12 -- OchaCaml: -- let f2 x = reset (fun () -> if shift (fun k -> k) then 1 else 2) x;; f2 = reset (if shift (\k -> return k) then 1 else 2) f2r = run (f2 \$: true) -- 1 -- in Haskell, we don't need eta-expand the definitions to avoid -- the value restriction {- bad = reset (3 + shift (\k -> true)) - 1 Couldn't match expected type `Int' with actual type `Prelude.Bool' Expected type: C Int Int Int Actual type: C Int Int Prelude.Bool In the expression: true In the first argument of `shift', namely `(\ k -> true)' -} -- The list-append example, which requires pattern-matching -- Pattern-matching in our EDSL is a bit ungainly -- OchaCaml: {- let rec id lst = match lst with [] -> shift (fun k -> k) | first :: rest -> first :: id rest ;; (* id : 'a list => 'a list = *) (* id : 'a list / 'b -> 'a list / ('a list -> 'b) = *) -} idl ls = ls >>= check where check [] = shift (\k -> return k) check (first:rest) = return first `cons` (idl (return rest)) -- Inferred type: -- idl :: C ([sigma] -> b) ([sigma] -> b) [sigma] -- -> C b ([sigma] -> b) [sigma] -- OchaCaml: {- let append lst = reset (fun () -> id [1; 2; 3]) lst ;; (* append : int list -> int list = *) -} append = reset (idl (1 `cons` 2 `cons` 3 `cons` nil)) -- append :: Prelude.Num sigma => C a a ([sigma] -> [sigma]) tapp = run (append \$: (4 `cons` 5 `cons` nil)) -- [1,2,3,4,5] -- ------------------------------------------------------------------------ -- The implementation: hiding the Monadish plumbing true, false :: (Monadish m) => m a a (Prelude.Bool) true = return Prelude.True false = return Prelude.False -- Standard arithmetic infixl 6 +,- infixl 7 * (+),(-),(*) :: (Monadish m) => m b1 b Int -> m b g Int -> m b1 g Int x + y = ((Prelude.+) `appure` x ) \$: y x - y = ((Prelude.-) `appure` x ) \$: y x * y = ((Prelude.*) `appure` x ) \$: y fromInteger = return . Prelude.fromInteger ifThenElse e1 e2 e3 = e1 >>= \x -> case x of {Prelude.True -> e2; _ -> e3} -- define the standard `monadic' operations -- to be monadish instead m >>= f = m >== f return x = ret x fail x = Prelude.error x f =<< m = m >>= f infixr 5 `cons` cons x y = ((:) `appure` x) \$: y nil = return [] appure f m = m >>= \x -> return (f x) infixr 0 \$: f \$: m = do xv <- m fv <- f return (fv xv)