[Haskell-cafe] Re: Flipping *->*->* kinds, or monadic
finally-tagless madness
Edward Kmett
ekmett at gmail.com
Thu Jul 2 20:15:52 EDT 2009
Actually the problem lies in your definition of fz, it has the wrong type to
be used in lam.
The Z you get out of fz as type Z b String, but you need it to have Z (a ->
b) String so that when you strip off the Z you have a Y String (a -> b)
matching the result type of lam.
To get there replace your definition of fz with:
> fz :: Z a String -> Z (a -> b) String
> fz = Z . Y . unY . f . unZ
In 6.10.2 I used {-# LANGUAGE FlexibleInstances, TypeSynonymInstances,
MultiParamTypeClasses, ScopedTypeVariables #-}
and that compiled just fine.
On Thu, Jul 2, 2009 at 8:02 PM, Ahn, Ki Yung <kyagrd at gmail.com> wrote:
> Kim-Ee Yeoh wrote:
>
>>
>> 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?
>>
>
> Not an answer, but just a different error message from GHC 6.10.3 when I
> tried loading up your code.
>
> kyagrd at kyavaio:~/tmp$ ghci EvalTaglessF.hs
> GHCi, version 6.10.3: http://www.haskell.org/ghc/ :? for help
> Loading package ghc-prim ... linking ... done.
> Loading package integer ... linking ... done.
> Loading package base ... linking ... done.
> [1 of 1] Compiling Main ( EvalTaglessF.hs, interpreted )
>
> EvalTaglessF.hs:264:14:
> Couldn't match expected type `b1' against inferred type `b'
> `b1' is a rigid type variable bound by
> the type signature for `fz' at EvalTaglessF.hs:263:31
> `b' is a rigid type variable bound by
> the type signature for `lam' at EvalTaglessF.hs:248:26
> Expected type: Z b1 String
> Inferred type: Z b String
> In the expression: Z . f . unZ
> In the definition of `fz': fz = Z . f . unZ
>
> EvalTaglessF.hs:264:22:
> Couldn't match expected type `a1' against inferred type `a'
> `a1' is a rigid type variable bound by
> the type signature for `fz' at EvalTaglessF.hs:263:17
> `a' is a rigid type variable bound by
> the type signature for `lam' at EvalTaglessF.hs:248:16
> Expected type: Z a1 String
> Inferred type: Z a String
> In the second argument of `(.)', namely `unZ'
> In the second argument of `(.)', namely `f . unZ'
> Failed, modules loaded: none.
>
>
>
> I hope this gives you a hint, if any. I am not exactly sure about how to
> solve this but I might try using scoped type variables extension somehow if
> I were in your shoe.
>
>
> _______________________________________________
> 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/08e1cf0e/attachment.html
More information about the Haskell-Cafe
mailing list