[Haskell-cafe] Flipping *->*->* kinds, or monadic finally-tagless madness

[Kim-Ee Yeoh]

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.