[Haskell-cafe] Flipping *->*->* kinds, or monadic finally-tagless
madness
Edward Kmett
ekmett at gmail.com
Thu Jul 2 21:49:18 EDT 2009
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.biurvOir4 at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090702/0348a65a/attachment.html
More information about the Haskell-Cafe
mailing list