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
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-tagle... 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