Magicloud Magiclouds | 21 Aug 08:36 2014
Picon

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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Dominique Devriese | 21 Aug 08:47 2014
Picon

Re: Why this existential type could not work?

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 <at> 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 <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Magicloud Magiclouds | 21 Aug 09:08 2014
Picon

Re: Why this existential type could not work?

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 <at> 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 <at> 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 <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



--
竹密岂妨流水过
山高哪阻野云飞

And for G+, please use magiclouds#gmail.com.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Albert Y. C. Lai | 22 Aug 19:08 2014
Picon

Re: Why this existential type could not work?

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.
Swierstra, S.D. | 22 Aug 23:40 2014
Picon

Re: Why this existential type could not work?


On 21 Aug 2014, at 9:08 , Magicloud Magiclouds <magicloud.magiclouds <at> gmail.com> wrote:

Thank you. I think I need to understand the different means of forall when it at different positions.

The forall in this case should be "pronounced" as "exists"; reusing the keyword forall was clearly an unfortunate decision.

When should either write:


  data Sealed where
    Sealed :: forall a. SomeClass a => TVar a -> Sealed


or 

data Sealed = exists a . SomeClass a=>   Sealed (TVar a)

In the former notation the emphasis is on Sealed being used to construct a value, whereas in the second case the emphasis is more on its role as a constituent of a pattern.

    Doaitse




On Thu, Aug 21, 2014 at 2:47 PM, Dominique Devriese <dominique.devriese <at> 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 <at> 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 <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



--
竹密岂妨流水过
山高哪阻野云飞

And for G+, please use magiclouds#gmail.com.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Philipp Stephani | 21 Aug 09:51 2014
Picon

Re: Why this existential type could not work?



Magicloud Magiclouds <magicloud.magiclouds <at> gmail.com> schrieb am Thu Aug 21 2014 at 08:37:09:
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 }
 
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane