限定継続なし版

http://www.tom.sfc.keio.ac.jp/~sakai/d/?date=20100124#p01
特に何がやりたい、とかは無かったんですけど限定継続の型がどないや!!っていうのを埋め込んで調べてみたかったのでというのがありました。
それでつまらない事を雑談会の時に話してしまったので、さかいさんの手を煩わせる事になってすいません。

取りあえず実行する所まで含めて、Felleisen's C-operatorとcall/ccを持つ型付きのDSLは下のような感じになりました。
ex5ではerror使ってるくせに、ex7ではEither( Or みたいなもんです )使って良い子ちゃんぶりやがって!!みたいなのは・・・。
そういうのも良いんじゃ無いでしょうか。

{-# LANGUAGE GADTs #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NoMonomorphismRestriction #-}

data Void where
    Void :: String -> Void

instance Show Void where
    show (Void s) = show s

data Exp ty where
    EInt :: Int -> Exp Int
    ELam :: (a -> b) -> Exp (a -> b)
    EApp :: Exp (a -> b) -> Exp a -> Exp b
    C :: Exp ((a -> Void) -> Void) -> Exp a
    CallWithCC :: Exp ((a -> Void) -> Either Void a) -> Exp a

instance Show (Exp ty) where
    show (EInt i) = show i
    show (ELam f) = "ELam"
    show (EApp f arg) = "EApp : " ++ show f ++ " " ++ show arg
    show (C k) = "C : " ++ show k

app :: Exp (e -> Void) -> e -> Void
app (ELam f) i = f i

cps :: Exp e -> Exp (e -> Void) -> Void
cps (EInt i) k = app k i
cps (ELam f) k = app k f
cps (EApp (f :: Exp (a -> e)) (arg :: Exp a) :: Exp e) (k :: Exp (e -> Void)) = cps f k'
    where
      k' :: Exp ((a -> e) -> Void)
      k' = ELam (\f' -> cps arg (ELam (\arg' -> app k (f' arg'))))
cps (C klam) k = cps (EApp klam k) (ELam id)
cps (CallWithCC (klam :: Exp ((e -> Void) -> Either Void e))) (k :: Exp (e -> Void)) = cps (EApp klam k) k'
    where
      k' :: Exp (Either Void e -> Void)
      k' = ELam k'_impl
          where
            k'_impl (Right r) = app k r
            k'_impl (Left x) = x

exit = ELam (\v -> Void $ show v)

ex1 = cps (EInt 42) exit
ex2 = cps (EApp (ELam (\a -> 42 + a)) (EInt 42)) exit
ex3 = cps (EApp (EApp (ELam (\l -> (\r -> l + r))) (EInt 41)) (EInt 1)) exit
ex4 = cps (EApp (ELam (\x -> x + 1)) (C (ELam (\k -> k 1)))) exit
ex5 = cps (EApp (ELam (\x -> x + 1)) (C (ELam (\k -> error $ show 1)))) exit
ex6 = cps (EApp (ELam (\x -> x + 1)) (CallWithCC (ELam (\k -> Left $ k 1)))) exit
ex7 = cps (EApp (ELam (\x -> x + 1)) (CallWithCC (ELam (\k -> Right 1)))) exit

はVoidを所々決め打しちゃえば悲しい事にはならなくて、でもまぁunsafe*とかを許すならば、cpsの型を(Exp e) → Exp (e → ret) → Exp retとかにしてしまって、Coperatorとcall/ccで使ってshift/reset側で型が少しでも安全になりますよーに!!とかすれば良いんじゃないかなぁという気もするし、所でOlegさんがFLOPS2010で発表する話を先に読んだ方が良い気がして来たけどあれはかなり頑張る書き方に成ってる気がするのでDSLとかじゃないぽいなぁと思ったけど別に頑張るものだからDSLじゃないとかっていう話になるわけないしというかこれは逆に手を抜き過ぎで、ところでこのように一文が大変長い物は良く無い。