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

Kim-Ee Yeoh a.biurvOir4 at asuhan.com
Thu Jul 2 17:52:27 EDT 2009


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.



More information about the Haskell-Cafe mailing list