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

[Edward Kmett]

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