Why this existential type could not work?
Hi, For example, code like this: newtype Sealed = Sealed { unSealed :: forall a. SomeClass a => TVar a } mkSealed :: (SomeClass a) => a -> IO Sealed mkSealed = fmap Sealed . newTVarIO When compiling, I would get: Expected type: a -> IO (forall a1. SomeClass a1 => TVar a1) Actual type: a -> IO (TVar a) How to correctly restrict type parameter a here? -- 竹密岂妨流水过 山高哪阻野云飞 And for G+, please use magiclouds#gmail.com.
Dear Magicloud,
What you're writing is not an existential type. The syntax you used
meant that Sealed wraps a value of type "forall a. SomeClass a => TVar
a", while you wanted to say that it should contain a value of type
"TVar a" for some a that satisfies SomeClass, i.e. an existential
type. Below is what I think you want:
Regards,
Dominique
{-# LANGUAGE RankNTypes, GADTs #-}
module Test where
import GHC.Conc
class SomeClass a
data Sealed where
Sealed :: forall a. SomeClass a => TVar a -> Sealed
mkSealed :: (SomeClass a) => a -> IO Sealed
mkSealed = fmap Sealed . newTVarIO
2014-08-21 8:36 GMT+02:00 Magicloud Magiclouds
Hi,
For example, code like this:
newtype Sealed = Sealed { unSealed :: forall a. SomeClass a => TVar a }
mkSealed :: (SomeClass a) => a -> IO Sealed mkSealed = fmap Sealed . newTVarIO
When compiling, I would get:
Expected type: a -> IO (forall a1. SomeClass a1 => TVar a1) Actual type: a -> IO (TVar a)
How to correctly restrict type parameter a here?
-- 竹密岂妨流水过 山高哪阻野云飞
And for G+, please use magiclouds#gmail.com.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Thank you. I think I need to understand the different means of forall when it at different positions. On Thu, Aug 21, 2014 at 2:47 PM, Dominique Devriese < dominique.devriese@cs.kuleuven.be> wrote:
Dear Magicloud,
What you're writing is not an existential type. The syntax you used meant that Sealed wraps a value of type "forall a. SomeClass a => TVar a", while you wanted to say that it should contain a value of type "TVar a" for some a that satisfies SomeClass, i.e. an existential type. Below is what I think you want:
Regards, Dominique
{-# LANGUAGE RankNTypes, GADTs #-}
module Test where
import GHC.Conc
class SomeClass a
data Sealed where Sealed :: forall a. SomeClass a => TVar a -> Sealed
mkSealed :: (SomeClass a) => a -> IO Sealed mkSealed = fmap Sealed . newTVarIO
2014-08-21 8:36 GMT+02:00 Magicloud Magiclouds < magicloud.magiclouds@gmail.com>:
Hi,
For example, code like this:
newtype Sealed = Sealed { unSealed :: forall a. SomeClass a => TVar a }
mkSealed :: (SomeClass a) => a -> IO Sealed mkSealed = fmap Sealed . newTVarIO
When compiling, I would get:
Expected type: a -> IO (forall a1. SomeClass a1 => TVar a1) Actual type: a -> IO (TVar a)
How to correctly restrict type parameter a here?
-- 竹密岂妨流水过 山高哪阻野云飞
And for G+, please use magiclouds#gmail.com.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- 竹密岂妨流水过 山高哪阻野云飞 And for G+, please use magiclouds#gmail.com.
On 14-08-21 03:08 AM, Magicloud Magiclouds wrote:
Thank you. I think I need to understand the different means of forall when it at different positions.
Each value has a giver (aka creator, implementer) and a receiver (aka user, client). It always and only comes down to: who chooses what to plug into the type variable, the giver or the receiver. Exactly one of the two can choose. data Head = HC (forall b. Maybe b) head_example :: Head head_example = HC (...) The receiver of head_example can choose what b is. The giver of head_example cannot choose. How do I know? Because this is analogous to: like_head_example :: forall b. Maybe b like_head_example = ... The giver of like_head_example cannot choose. data Tail = forall b. TC (Maybe b) tail_example :: Tail tail_example = TC (...) The giver of tail_example can choose what b is. The receiver cannot choose. How do I know? Because the type of TC is TC :: forall b. Maybe b -> Tail The user of TC can choose. The user of TC is the giver of tail_example. Now I talk about parametricity. Parametricity implies: the person who cannot choose cannot ask either. The giver of head_example cannot choose b. He/She cannot ask what is chosen either. The receiver of tail_example cannot choose b. He/She cannot ask what is chosen either. Non-generic Java lacks parametricity. Therefore, the person who cannot choose can still ask what is chosen by instanceOf. Generic Java has parametricity. Like Haskell, the person who cannot choose cannot ask by instanceOf.
On 21 Aug 2014, at 9:08 , Magicloud Magiclouds
Hi,
For example, code like this:
newtype Sealed = Sealed { unSealed :: forall a. SomeClass a => TVar a }
mkSealed :: (SomeClass a) => a -> IO Sealed mkSealed = fmap Sealed . newTVarIO
When compiling, I would get:
Expected type: a -> IO (forall a1. SomeClass a1 => TVar a1) Actual type: a -> IO (TVar a)
How to correctly restrict type parameter a here?
-- 竹密岂妨流水过 山高哪阻野云飞
And for G+, please use magiclouds#gmail.comhttp://gmail.com/.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.orgmailto:Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- 竹密岂妨流水过 山高哪阻野云飞 And for G+, please use magiclouds#gmail.comhttp://gmail.com/. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.orgmailto:Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Magicloud Magiclouds
Hi,
For example, code like this:
newtype Sealed = Sealed { unSealed :: forall a. SomeClass a => TVar a }
I think this should be written as data Sealed = forall a. SomeClass a => Sealed { unSealed :: TVar a }
participants (5)
-
Albert Y. C. Lai -
Dominique Devriese -
Magicloud Magiclouds -
Philipp Stephani -
Swierstra, S.D.