You might also look at doing it without all the State monad noise with something like:<div><br></div><div><div>> class Symantics repr where</div><div>> int :: Int -> repr Int</div><div>> add :: repr Int -> repr Int -> repr Int</div>
<div>> lam :: (repr a -> repr b) -> repr (a->b)</div><div>> app :: repr (a -> b) -> repr a -> repr b</div><div><br></div><div>> newtype Pretty a = Pretty { runPretty :: [String] -> String } </div>
<div><br></div><div>> pretty :: Pretty a -> String</div><div>> pretty (Pretty f) = f vars where</div><div>> vars = [ [i] | i <- ['a'..'z']] ++ [i : show j | j <- [1..], i <- ['a'..'z'] ]</div>
<div><br></div><div>> instance Symantics Pretty where</div><div>> int = Pretty . const . show</div><div>> add x y = Pretty $ \vars -> "(" ++ runPretty x vars ++ " + " ++ runPretty y vars ++ ")"</div>
<div>> lam f = Pretty $ \ (v:vars) -> "(\\" ++ v ++ ". " ++ runPretty (f (var v)) vars ++ ")" where</div><div>> var = Pretty . const</div><div>> app f x = Pretty $ \vars -> "(" ++ runPretty f vars ++ " " ++ runPretty x vars ++ ")"</div>
<div><br></div><div>-Edward Kmett</div><div><br><div class="gmail_quote">On Thu, Jul 2, 2009 at 5:52 PM, Kim-Ee Yeoh <span dir="ltr"><<a href="mailto:a.biurvOir4@asuhan.com">a.biurvOir4@asuhan.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"><br>
I'm trying to write HOAS Show instances for the finally-tagless<br>
type-classes using actual State monads.<br>
<br>
The original code:<br>
<a href="http://okmij.org/ftp/Computation/FLOLAC/EvalTaglessF.hs" target="_blank">http://okmij.org/ftp/Computation/FLOLAC/EvalTaglessF.hs</a><br>
<br>
Two type variables are needed: one to vary over the Symantics<br>
class (but only as a phantom type) and another to vary over the<br>
Monad class. Hence, the use of 2-variable type constructors.<br>
<br>
> type VarCount = int<br>
> newtype Y b a = Y {unY :: VarCount -> (b, VarCount)}<br>
<br>
Not knowing of a type-level 'flip', I resort to newtype isomorphisms:<br>
<br>
> newtype Z a b = Z {unZ :: Y b a}<br>
> instance Monad (Z a) where<br>
> return x = Z $ Y $ \c -> (x,c)<br>
> (Z (Y m)) >>= f = Z $ Y $ \c0 -> let (x,c1) = m c0 in (unY . unZ) (f<br>
> x) c1 -- Pace, too-strict puritans<br>
> instance MonadState String (Z a) where<br>
> get = Z $ Y $ \c -> (show c, c)<br>
> put x = Z $ Y $ \_ -> ((), read x)<br>
<br>
So far so good. Now for the Symantics instances (abridged).<br>
<br>
> class Symantics repr where<br>
> int :: Int -> repr Int -- int literal<br>
> add :: repr Int -> repr Int -> repr Int<br>
> lam :: (repr a -> repr b) -> repr (a->b)<br>
<br>
> instance Symantics (Y String) where<br>
> int = unZ . return . show<br>
> add x y = unZ $ do<br>
> sx <- Z x<br>
> sy <- Z y<br>
> return $ "(" ++ sx ++ " + " ++ sy ++ ")"<br>
<br>
The add function illustrates the kind of do-sugaring we know and love<br>
that I want to use for Symantics.<br>
<br>
> lam f = unZ $ do<br>
> show_c0 <- get<br>
> let<br>
> vname = "v" ++ show_c0<br>
> c0 = read show_c0 :: VarCount<br>
> c1 = succ c0<br>
> fz :: Z a String -> Z b String<br>
> fz = Z . f . unZ<br>
> put (show c1)<br>
> s <- (fz . return) vname<br>
> return $ "(\\" ++ vname ++ " -> " ++ s ++ ")"<br>
<br>
Now with lam, I get this cryptic error message (under 6.8.2):<br>
<br>
Occurs check: cannot construct the infinite type: b = a -> b<br>
When trying to generalise the type inferred for `lam'<br>
Signature type: forall a1 b1.<br>
(Y String a1 -> Y String b1) -> Y String (a1 -><br>
b1)<br>
Type to generalise: forall a1 b1.<br>
(Y String a1 -> Y String b1) -> Y String (a1 -><br>
b1)<br>
In the instance declaration for `Symantics (Y String)'<br>
<br>
Both the two types in the error message are identical, which suggests<br>
no generalization is needed. I'm puzzled why ghc sees an infinite type.<br>
<br>
Any ideas on how to proceed?<br>
<font color="#888888"><br>
--<br>
View this message in context: <a href="http://www.nabble.com/Flipping-*-%3E*-%3E*-kinds%2C-or-monadic-finally-tagless-madness-tp24314553p24314553.html" target="_blank">http://www.nabble.com/Flipping-*-%3E*-%3E*-kinds%2C-or-monadic-finally-tagless-madness-tp24314553p24314553.html</a><br>
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</font></blockquote></div><br></div></div>