Hi, I'm writing some database code using HSQL and had to stop on a problem with rank-2-polymorphism that I can't solve. The essence of my code is: module Value where import Data.Maybe class SqlBind a where fromSqlValue :: String -> a data Field data Value emptyValue :: Field -> Value emptyValue _ = ... readValue :: Field -> (forall s. SqlBind s => s) -> Value readValue _ = ... That works just fine. But now I want a version of readValue that has a Maybe wrapped around the second parameter and that shall call readValue in the case of a Just and emptyValue in the case of Nothing. But I can't figure out how to write this function as I always get compiler errors. My trials were: -- The type I want to get. readValue' :: Field -> (forall s. SqlBind s => Maybe s) -> Value -- First trial: readValue' fld s = if isJust s then readValue fld (fromJust s) else emptyValue fld -- Second trial: readValue' fld s | isJust s = readValue fld (fromJust s) | otherwise = emptyValue fld -- Third trial: readValue' fld (Just s) = readValue fld s readValue' fld Nothing = emptyValue fld -- Fourth trial: readValue fld s = case s of Just s' -> readValue fld s' Nothing -> emptyValue fld But none of these trials worked. Is there any solution that works with GHC-6.6 for now? Thanks in advance, Martin.
On Fri, Mar 23, 2007 at 02:18:50PM +0100, Martin Huschenbett wrote:
-- The type I want to get. readValue' :: Field -> (forall s. SqlBind s => Maybe s) -> Value
-- First trial: readValue' fld s = if isJust s then readValue fld (fromJust s) else emptyValue fld
Is there a reason you don't want this?: readValue' :: Field -> Maybe (forall s. SqlBind s => s) -> Value readValue' fld s = if isJust s then readValue fld (fromJust s) else emptyValue fld Thanks Ian
Ian Lynagh schrieb:
readValue' :: Field -> Maybe (forall s. SqlBind s => s) -> Value readValue' fld s = if isJust s then readValue fld (fromJust s) else emptyValue fld
Thank you very much, that's exactly what I wanted. After reading in the GHC users guide about rank 2 polymorphism I thought that this is not possible. Chapter "7.4.8. Arbitrary-rank polymorphism" says: There is one place you cannot put a forall: you cannot instantiate a type variable with a forall-type. So you cannot make a forall-type the argument of a type constructor. So these types are illegal: x1 :: [forall a. a->a] x2 :: (forall a. a->a, Int) x3 :: Maybe (forall a. a->a) Maybe the users guide is not precise enough at this point. Regards, Martin.
Hello, What Ian suggested is a very GHC 6.6 specific solution that uses much more that simply rank-2 types. Here is another solution that uses just rank-2 types (and, by the way, all type signatures are optional, as in ordinary Haskell): module Value where class SqlBind a where fromSqlValue :: String -> a data Field data Value emptyValue :: Field -> Value emptyValue _ = undefined data Binder = Binder (forall s. SqlBind s => s) readValue :: Field -> Binder -> Value readValue _ (Binder _) = undefined readOptValue :: Field -> Maybe Binder -> Value readOptValue f x = maybe (emptyValue f) (readValue f) x Hope this helps -Iavor
Hi again, the solutions/proposals of Ian and Iavor seem to be exactly what I need at a first glance. But looking at them more in detail reveals some other problems. I also have got a function
getFieldValueMB :: SqlBind s => Statement -> String -> Maybe s
To get Ians approach working I would need a function of type
getFieldValueMB' :: Statement -> String -> Maybe (forall s. SqlBind s => s)
and for Iavor approach I would need a function of type:
getFieldValueMB' :: Statament -> String -> Maybe Binder
which are almost the same. The remaining problem is: How can I construct either of these functions? My thoughts were that for any class C the types
Maybe (forall a. C a => a) (I will call it T1 for short)
and
(forall a. C a => Maybe a) (I will call it T2 for short)
are isomorphic. Defining the isomorphism from T1 to T2 is quite simple: iso1 :: Maybe (forall a. C a => a) -> (forall a. C a => Maybe a) iso1 (Just s) = Just s iso1 Nothing = Nothing But I don't catch how to define the isomorphism of the other direction (from T2 to T1). I would guess that defining this isomorphism would also solve my problem concerning the SQL stuff. So, is there anybody who knows how to define this isomorphism in a way that GHC-6.6 can compile it? Thanks for you help in advance, Martin.
Martin Huschenbett schrieb:
My thoughts were that for any class C the types
Maybe (forall a. C a => a) (I will call it T1 for short)
and
(forall a. C a => Maybe a) (I will call it T2 for short)
are isomorphic. Defining the isomorphism from T1 to T2 is quite simple:
iso1 :: Maybe (forall a. C a => a) -> (forall a. C a => Maybe a) iso1 (Just s) = Just s iso1 Nothing = Nothing
But I don't catch how to define the isomorphism of the other direction (from T2 to T1). I would guess that defining this isomorphism would also solve my problem concerning the SQL stuff.
I found the solution to my problem. I just want to post it for others who may come across the same problem. The trick was simply looking at GHC's error message that tells something about ambiguous types. So let T be an arbitrary instance of C then the other isomorphism becomes:
iso2 :: (forall a. C a => Maybe a) -> Maybe (forall a. C a => a) iso2 s if isJust (s :: Maybe T) then Just (fromJust s) else Nothing
Regards, Martin.
Hello Martin, Friday, March 23, 2007, 11:37:16 PM, you wrote:
readValue' :: Field -> Maybe (forall s. SqlBind s => s) -> Value
Thank you very much, that's exactly what I wanted. After reading in the GHC users guide about rank 2 polymorphism I thought that this is not possible. Chapter "7.4.8. Arbitrary-rank polymorphism" says:
"impredicative polymorphism" is new in ghc 6.6. look for this word in ghc docs and in spj's papers -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
Martin Huschenbett wrote:
readValue :: Field -> (forall s. SqlBind s => s) -> Value readValue _ = ...
That works just fine. But now I want a version of readValue that has a Maybe wrapped around the second parameter and that shall call readValue in the case of a Just and emptyValue in the case of Nothing. But I can't figure out how to write this function as I always get compiler errors.
-- The type I want to get. readValue' :: Field -> (forall s. SqlBind s => Maybe s) -> Value [..] -- Fourth trial: readValue fld s = case s of Just s' -> readValue fld s' Nothing -> emptyValue fld
For me, the fourth trial works, at least on f :: (forall s . Num s => Maybe s) -> Int f y = case y of Just x -> x Nothing -> 0 Your definition has a typo (missing tick '), maybe that's the cause why it doesn't work? Furthermore, I guess that let-binding any troublesome rank-2-variables is beneficial. Regards, apfelmus
apfelmus schrieb:
For me, the fourth trial works, at least on
f :: (forall s . Num s => Maybe s) -> Int f y = case y of Just x -> x Nothing -> 0
This works, because the compiler knows that x has to have type Int. But if you want to apply a function g :: (forall a. Num a => a) -> Int to x before returning, it doesn't work any more. But I need this function application. However, thanks for your help. Regards, Martin.
participants (5)
-
apfelmus -
Bulat Ziganshin -
Ian Lynagh -
Iavor Diatchki -
Martin Huschenbett