[Haskell-cafe] Flipping *->*->* kinds, or monadic
finally-tagless madness
Kim-Ee Yeoh
a.biurvOir4 at asuhan.com
Fri Jul 3 12:58:57 EDT 2009
Hi Edward,
Your runPretty version fits the bill nicely, thank you. I might still retain
the state monad version because it allows generalizations beyond
pretty-printing.
As for fixing the original bug, I've found that the real magic lies
in the incantation (Y . unY) inserted at the appropriate places. Indeed,
I've removed type signatures because try as I might, I couldn't
write something the type-checker would accept. This is for 6.8.2.
FWIW, the final version:
instance Symantics (Y String) where
int = unZ . return . show
bool = unZ . return . show
lam f = unZ $ do
show_c0 <- get
let
vname = "v" ++ show_c0
c0 = read show_c0 :: VarCount
c1 = succ c0
put (show c1)
bodyf <- (Z . Y . unY . f . unZ . return) vname
return $ "(\\" ++ vname ++ " -> " ++ bodyf ++ ")"
fix f = pr3 [MkZa $ lam f] ["(fix ", ")"]
app e1 e2 = pr3 [MkZa e1,MkZa e2] ["("," " ,")"]
add e1 e2 = pr3 [MkZa e1,MkZa e2] ["("," + " ,")"]
mul e1 e2 = pr3 [MkZa e1,MkZa e2] ["("," * " ,")"]
leq e1 e2 = pr3 [MkZa e1,MkZa e2] ["("," <= ",")"]
if_ be et ee = pr3 [MkZa be,MkZa et,MkZa ee] ["(if "," then "," else
",")"]
-- Suppress the Symantics phantom type by casting to an existential
data Za where
MkZa :: Y String a -> Za
pr3 a b = unZ $ pr2 a b
pr2 :: forall a. [Za] -> [String] -> Z a String
pr2 _ [] = return ""
pr2 [] ts = (return . concat) ts
pr2 ((MkZa e):es) (t:ts) = do
s1 <- (Z . Y . unY) e -- that (Y . unY) magical
incantation again!
s2 <- pr2 es ts
return $ t ++ s1 ++ s2
Edward Kmett wrote:
>
> You might also look at doing it without all the State monad noise with
> something like:
>> class Symantics repr where
>> int :: Int -> repr Int
>> add :: repr Int -> repr Int -> repr Int
>> lam :: (repr a -> repr b) -> repr (a->b)
>> app :: repr (a -> b) -> repr a -> repr b
>
>> newtype Pretty a = Pretty { runPretty :: [String] -> String }
>
>> pretty :: Pretty a -> String
>> pretty (Pretty f) = f vars where
>> vars = [ [i] | i <- ['a'..'z']] ++ [i : show j | j <- [1..], i <-
> ['a'..'z'] ]
>
>> instance Symantics Pretty where
>> int = Pretty . const . show
>> add x y = Pretty $ \vars -> "(" ++ runPretty x vars ++ " + " ++
> runPretty y vars ++ ")"
>> lam f = Pretty $ \ (v:vars) -> "(\\" ++ v ++ ". " ++ runPretty (f (var
> v)) vars ++ ")" where
>> var = Pretty . const
>> app f x = Pretty $ \vars -> "(" ++ runPretty f vars ++ " " ++
>> runPretty
> x vars ++ ")"
>
--
View this message in context: http://www.nabble.com/Flipping-*-%3E*-%3E*-kinds%2C-or-monadic-finally-tagless-madness-tp24314553p24326046.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
More information about the Haskell-Cafe
mailing list