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 ++ ")" -Edward Kmett On Thu, Jul 2, 2009 at 5:52 PM, Kim-Ee Yeoh <a.biurvo...@asuhan.com> wrote: > > I'm trying to write HOAS Show instances for the finally-tagless > type-classes using actual State monads. > > The original code: > http://okmij.org/ftp/Computation/FLOLAC/EvalTaglessF.hs > > Two type variables are needed: one to vary over the Symantics > class (but only as a phantom type) and another to vary over the > Monad class. Hence, the use of 2-variable type constructors. > > > type VarCount = int > > newtype Y b a = Y {unY :: VarCount -> (b, VarCount)} > > Not knowing of a type-level 'flip', I resort to newtype isomorphisms: > > > newtype Z a b = Z {unZ :: Y b a} > > instance Monad (Z a) where > > return x = Z $ Y $ \c -> (x,c) > > (Z (Y m)) >>= f = Z $ Y $ \c0 -> let (x,c1) = m c0 in (unY . unZ) (f > > x) c1 -- Pace, too-strict puritans > > instance MonadState String (Z a) where > > get = Z $ Y $ \c -> (show c, c) > > put x = Z $ Y $ \_ -> ((), read x) > > So far so good. Now for the Symantics instances (abridged). > > > class Symantics repr where > > int :: Int -> repr Int -- int literal > > add :: repr Int -> repr Int -> repr Int > > lam :: (repr a -> repr b) -> repr (a->b) > > > instance Symantics (Y String) where > > int = unZ . return . show > > add x y = unZ $ do > > sx <- Z x > > sy <- Z y > > return $ "(" ++ sx ++ " + " ++ sy ++ ")" > > The add function illustrates the kind of do-sugaring we know and love > that I want to use for Symantics. > > > lam f = unZ $ do > > show_c0 <- get > > let > > vname = "v" ++ show_c0 > > c0 = read show_c0 :: VarCount > > c1 = succ c0 > > fz :: Z a String -> Z b String > > fz = Z . f . unZ > > put (show c1) > > s <- (fz . return) vname > > return $ "(\\" ++ vname ++ " -> " ++ s ++ ")" > > Now with lam, I get this cryptic error message (under 6.8.2): > > Occurs check: cannot construct the infinite type: b = a -> b > When trying to generalise the type inferred for `lam' > Signature type: forall a1 b1. > (Y String a1 -> Y String b1) -> Y String (a1 -> > b1) > Type to generalise: forall a1 b1. > (Y String a1 -> Y String b1) -> Y String (a1 -> > b1) > In the instance declaration for `Symantics (Y String)' > > Both the two types in the error message are identical, which suggests > no generalization is needed. I'm puzzled why ghc sees an infinite type. > > Any ideas on how to proceed? > > -- > View this message in context: > http://www.nabble.com/Flipping-*-%3E*-%3E*-kinds%2C-or-monadic-finally-tagless-madness-tp24314553p24314553.html > Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe