pattern match on forall'ed data

newer
Munich Haskell Meeting, 2016-07-27...

older
Re: [Haskell-cafe] Practical use...

Corentin Dupont

20 Jul 2016 20 Jul '16

11:18 a.m.

Hi all, I'm surprised this doesn't work: data SomeData = forall e. (Typeable e, Eq e) => SomeData e (===) :: (Typeable a, Typeable b, Eq a, Eq b) => a -> b -> Bool (===) x y = cast x == Just y test :: SomeData' -> Bool test (SomeData' e) | e === Nothing = True test _ = False It says Could not deduce (Eq a1) arising from a use of ‘===’ How can I achieve something of the same effect? Thanks Corentin

Attachments:

attachment.html (text/html — 714 bytes)

Show replies by date

Patrick Chilton

20 Jul 20 Jul

11:44 a.m.

It's because you're doing === Nothing and the type of the Nothing is ambiguous (Maybe a1). On Wed, Jul 20, 2016 at 5:18 PM, Corentin Dupont wrote:

...

Hi all, I'm surprised this doesn't work:

data SomeData = forall e. (Typeable e, Eq e) => SomeData e

(===) :: (Typeable a, Typeable b, Eq a, Eq b) => a -> b -> Bool (===) x y = cast x == Just y

test :: SomeData' -> Bool test (SomeData' e) | e === Nothing = True test _ = False

It says Could not deduce (Eq a1) arising from a use of ‘===’

How can I achieve something of the same effect?

Thanks Corentin

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Corentin Dupont

12:30 p.m.

I see.... The think is, I am interested to know if "e" is "Nothing", whatever the type of Nothing is! On Wed, Jul 20, 2016 at 5:44 PM, Patrick Chilton wrote:

...

It's because you're doing === Nothing and the type of the Nothing is ambiguous (Maybe a1).

On Wed, Jul 20, 2016 at 5:18 PM, Corentin Dupont < corentin.dupont@gmail.com> wrote:

...
Hi all, I'm surprised this doesn't work:

data SomeData = forall e. (Typeable e, Eq e) => SomeData e

(===) :: (Typeable a, Typeable b, Eq a, Eq b) => a -> b -> Bool (===) x y = cast x == Just y

test :: SomeData' -> Bool test (SomeData' e) | e === Nothing = True test _ = False

It says Could not deduce (Eq a1) arising from a use of ‘===’

How can I achieve something of the same effect?

Thanks Corentin

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Michael Burge

1:40 p.m.

I've used toConstr from Data.Data when I only care which constructor a value was constructed with. The specific type 'a' in 'Maybe a' is effectively a phantom type for the Nothing constructor, which I haven't used before. But it looks like it still works, so you could try comparing the constructors: Prelude Data.Typeable Data.Data> toConstr (Nothing :: Maybe Int) == toConstr (Nothing :: Maybe String) True Most of the time, you should be able to use a typeclass for this. On Wed, Jul 20, 2016 at 9:30 AM, Corentin Dupont wrote:

...

I see.... The think is, I am interested to know if "e" is "Nothing", whatever the type of Nothing is!

On Wed, Jul 20, 2016 at 5:44 PM, Patrick Chilton wrote:

...
It's because you're doing === Nothing and the type of the Nothing is ambiguous (Maybe a1).

On Wed, Jul 20, 2016 at 5:18 PM, Corentin Dupont < corentin.dupont@gmail.com> wrote:

...
Hi all, I'm surprised this doesn't work:

data SomeData = forall e. (Typeable e, Eq e) => SomeData e

(===) :: (Typeable a, Typeable b, Eq a, Eq b) => a -> b -> Bool (===) x y = cast x == Just y

test :: SomeData' -> Bool test (SomeData' e) | e === Nothing = True test _ = False

It says Could not deduce (Eq a1) arising from a use of ‘===’

How can I achieve something of the same effect?

Thanks Corentin

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Ivan Lazar Miljenovic

5:21 p.m.

On 21 July 2016 at 02:30, Corentin Dupont wrote:

...

I see.... The think is, I am interested to know if "e" is "Nothing", whatever the type of Nothing is!

Data.Maybe.isNothing ?

...

On Wed, Jul 20, 2016 at 5:44 PM, Patrick Chilton wrote:

...
It's because you're doing === Nothing and the type of the Nothing is ambiguous (Maybe a1).

On Wed, Jul 20, 2016 at 5:18 PM, Corentin Dupont wrote:

...
Hi all, I'm surprised this doesn't work:

data SomeData = forall e. (Typeable e, Eq e) => SomeData e

(===) :: (Typeable a, Typeable b, Eq a, Eq b) => a -> b -> Bool (===) x y = cast x == Just y

test :: SomeData' -> Bool test (SomeData' e) | e === Nothing = True test _ = False

It says Could not deduce (Eq a1) arising from a use of ‘===’

How can I achieve something of the same effect?

Thanks Corentin

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

-- Ivan Lazar Miljenovic Ivan.Miljenovic@gmail.com http://IvanMiljenovic.wordpress.com

Corentin Dupont

21 Jul 21 Jul

3:51 a.m.

Hi Ivan, I could use isNothing, but the data is forall'ed... I tried but it doesn't work: data SomeData = forall e. (Typeable e, Eq e) => SomeData e isNothing' :: SomeData -> Bool isNothing' (SomeData a) = case (cast a) of (a :: Maybe a) -> isNothing a Could not deduce (Typeable a) arising from a use of ‘cast’ On Wed, Jul 20, 2016 at 11:21 PM, Ivan Lazar Miljenovic < ivan.miljenovic@gmail.com> wrote:

...

On 21 July 2016 at 02:30, Corentin Dupont wrote:

...
I see.... The think is, I am interested to know if "e" is "Nothing", whatever the type of Nothing is!

Data.Maybe.isNothing ?

...
On Wed, Jul 20, 2016 at 5:44 PM, Patrick Chilton wrote:

...
It's because you're doing === Nothing and the type of the Nothing is ambiguous (Maybe a1).

On Wed, Jul 20, 2016 at 5:18 PM, Corentin Dupont wrote:

...
Hi all, I'm surprised this doesn't work:

data SomeData = forall e. (Typeable e, Eq e) => SomeData e

(===) :: (Typeable a, Typeable b, Eq a, Eq b) => a -> b -> Bool (===) x y = cast x == Just y

test :: SomeData' -> Bool test (SomeData' e) | e === Nothing = True test _ = False

It says Could not deduce (Eq a1) arising from a use of ‘===’

How can I achieve something of the same effect?

Thanks Corentin

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

-- Ivan Lazar Miljenovic Ivan.Miljenovic@gmail.com http://IvanMiljenovic.wordpress.com

Jonas Scholl

4:23 a.m.

If you want to use just Typeable, you can implement your own cast: Extract the TypeRep of the thing in SomeData, get the TyCon, which is the top-level constructor, i.e. Maybe without arguments, and compare it with the TyCon from Maybe. If they match, you coerce the value to Maybe () and use isNothing. While this is not completely safe, we do not evaluate the thing we just coerced to (), and thus are safe, as Maybe should have identical representation regardless of the type parameter. isNothing' :: SomeData -> Bool isNothing' (SomeData a) = tyCon == maybeTyCon && isNothing (unsafeCoerce a :: Maybe ()) where tyCon = typeRepTyCon (typeRep (mkProxy a)) maybeTyCon = typeRepTyCon $ typeRep (Proxy :: Proxy (Maybe ())) mkProxy :: a -> Proxy a mkProxy = const Proxy On 07/21/2016 09:51 AM, Corentin Dupont wrote:

...

Hi Ivan, I could use isNothing, but the data is forall'ed... I tried but it doesn't work:

data SomeData = forall e. (Typeable e, Eq e) => SomeData e

isNothing' :: SomeData -> Bool isNothing' (SomeData a) = case (cast a) of (a :: Maybe a) -> isNothing a

Could not deduce (Typeable a) arising from a use of ‘cast’

On Wed, Jul 20, 2016 at 11:21 PM, Ivan Lazar Miljenovic mailto:ivan.miljenovic@gmail.com> wrote:

On 21 July 2016 at 02:30, Corentin Dupont mailto:corentin.dupont@gmail.com> wrote: > I see.... > The think is, I am interested to know if "e" is "Nothing", whatever the type > of Nothing is!

Data.Maybe.isNothing ?

> > > > On Wed, Jul 20, 2016 at 5:44 PM, Patrick Chilton mailto:chpatrick@gmail.com> > wrote: >> >> It's because you're doing === Nothing and the type of the Nothing is >> ambiguous (Maybe a1). >> >> On Wed, Jul 20, 2016 at 5:18 PM, Corentin Dupont >> mailto:corentin.dupont@gmail.com> wrote: >>> >>> Hi all, >>> I'm surprised this doesn't work: >>> >>> data SomeData = forall e. (Typeable e, Eq e) => SomeData e >>> >>> (===) :: (Typeable a, Typeable b, Eq a, Eq b) => a -> b -> Bool >>> (===) x y = cast x == Just y >>> >>> test :: SomeData' -> Bool >>> test (SomeData' e) | e === Nothing = True >>> test _ = False >>> >>> It says >>> Could not deduce (Eq a1) arising from a use of ‘===’ >>> >>> How can I achieve something of the same effect? >>> >>> Thanks >>> Corentin >>> >>> _______________________________________________ >>> Haskell-Cafe mailing list >>> To (un)subscribe, modify options or view archives go to: >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe >>> Only members subscribed via the mailman list are allowed to post. >> >> > > > _______________________________________________ > Haskell-Cafe mailing list > To (un)subscribe, modify options or view archives go to: > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe > Only members subscribed via the mailman list are allowed to post.

-- Ivan Lazar Miljenovic Ivan.Miljenovic@gmail.com mailto:Ivan.Miljenovic@gmail.com http://IvanMiljenovic.wordpress.com

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Corentin Dupont

4:48 a.m.

That's great, exactly what I need. What do you mean by "just Typeable"? Do you have another idea in mind? On Thu, Jul 21, 2016 at 10:23 AM, Jonas Scholl wrote:

...

If you want to use just Typeable, you can implement your own cast: Extract the TypeRep of the thing in SomeData, get the TyCon, which is the top-level constructor, i.e. Maybe without arguments, and compare it with the TyCon from Maybe. If they match, you coerce the value to Maybe () and use isNothing. While this is not completely safe, we do not evaluate the thing we just coerced to (), and thus are safe, as Maybe should have identical representation regardless of the type parameter.

isNothing' :: SomeData -> Bool isNothing' (SomeData a) = tyCon == maybeTyCon && isNothing (unsafeCoerce a :: Maybe ()) where tyCon = typeRepTyCon (typeRep (mkProxy a)) maybeTyCon = typeRepTyCon $ typeRep (Proxy :: Proxy (Maybe ())) mkProxy :: a -> Proxy a mkProxy = const Proxy

On 07/21/2016 09:51 AM, Corentin Dupont wrote:

...
Hi Ivan, I could use isNothing, but the data is forall'ed... I tried but it doesn't work:

data SomeData = forall e. (Typeable e, Eq e) => SomeData e

isNothing' :: SomeData -> Bool isNothing' (SomeData a) = case (cast a) of (a :: Maybe a) -> isNothing a

Could not deduce (Typeable a) arising from a use of ‘cast’

On Wed, Jul 20, 2016 at 11:21 PM, Ivan Lazar Miljenovic mailto:ivan.miljenovic@gmail.com> wrote:

On 21 July 2016 at 02:30, Corentin Dupont mailto:corentin.dupont@gmail.com> wrote: > I see.... > The think is, I am interested to know if "e" is "Nothing", whatever the type > of Nothing is!

Data.Maybe.isNothing ?

> > > > On Wed, Jul 20, 2016 at 5:44 PM, Patrick Chilton mailto:chpatrick@gmail.com> > wrote: >> >> It's because you're doing === Nothing and the type of the Nothing is >> ambiguous (Maybe a1). >> >> On Wed, Jul 20, 2016 at 5:18 PM, Corentin Dupont >> mailto:corentin.dupont@gmail.com> wrote: >>> >>> Hi all, >>> I'm surprised this doesn't work: >>> >>> data SomeData = forall e. (Typeable e, Eq e) => SomeData e >>> >>> (===) :: (Typeable a, Typeable b, Eq a, Eq b) => a -> b -> Bool >>> (===) x y = cast x == Just y >>> >>> test :: SomeData' -> Bool >>> test (SomeData' e) | e === Nothing = True >>> test _ = False >>> >>> It says >>> Could not deduce (Eq a1) arising from a use of ‘===’ >>> >>> How can I achieve something of the same effect? >>> >>> Thanks >>> Corentin >>> >>> _______________________________________________ >>> Haskell-Cafe mailing list >>> To (un)subscribe, modify options or view archives go to: >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe >>> Only members subscribed via the mailman list are allowed to post. >> >> > > > _______________________________________________ > Haskell-Cafe mailing list > To (un)subscribe, modify options or view archives go to: > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe > Only members subscribed via the mailman list are allowed to post.

-- Ivan Lazar Miljenovic Ivan.Miljenovic@gmail.com mailto:Ivan.Miljenovic@gmail.com http://IvanMiljenovic.wordpress.com

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Jonas Scholl

5:26 a.m.

With "just Typeable" I mean using only the Typeable class. As already mentioned by Michael, it is also possible to achieve the same effect with the Data class: data SomeData = forall e. (Data e, Eq e) => SomeData e isNothing'' :: SomeData -> Bool isNothing'' (SomeData a) = toConstr a == toConstr (Nothing :: Maybe ()) Depending on your use-case, this may be simpler and it avoids using unsafeCoerce, which may make one feel a little bit uneasy. On the other hand, it adds an additional constraint. Additionally, a programmer can write his own Data instance while Typeable instances are always generated by the compiler (in newer versions of GHC). On 07/21/2016 10:48 AM, Corentin Dupont wrote:

...

That's great, exactly what I need. What do you mean by "just Typeable"? Do you have another idea in mind?

On Thu, Jul 21, 2016 at 10:23 AM, Jonas Scholl mailto:anselm.scholl@tu-harburg.de> wrote:

If you want to use just Typeable, you can implement your own cast: Extract the TypeRep of the thing in SomeData, get the TyCon, which is the top-level constructor, i.e. Maybe without arguments, and compare it with the TyCon from Maybe. If they match, you coerce the value to Maybe () and use isNothing. While this is not completely safe, we do not evaluate the thing we just coerced to (), and thus are safe, as Maybe should have identical representation regardless of the type parameter.

isNothing' :: SomeData -> Bool isNothing' (SomeData a) = tyCon == maybeTyCon && isNothing (unsafeCoerce a :: Maybe ()) where tyCon = typeRepTyCon (typeRep (mkProxy a)) maybeTyCon = typeRepTyCon $ typeRep (Proxy :: Proxy (Maybe ())) mkProxy :: a -> Proxy a mkProxy = const Proxy

On 07/21/2016 09:51 AM, Corentin Dupont wrote: > Hi Ivan, > I could use isNothing, but the data is forall'ed... > I tried but it doesn't work: > > data SomeData = forall e. (Typeable e, Eq e) => SomeData e > > isNothing' :: SomeData -> Bool > isNothing' (SomeData a) = case (cast a) of > (a :: Maybe a) -> isNothing a > > Could not deduce (Typeable a) arising from a use of ‘cast’ > > On Wed, Jul 20, 2016 at 11:21 PM, Ivan Lazar Miljenovic > mailto:ivan.miljenovic@gmail.com mailto:ivan.miljenovic@gmail.com>> wrote: > > On 21 July 2016 at 02:30, Corentin Dupont mailto:corentin.dupont@gmail.com > mailto:corentin.dupont@gmail.com>> wrote: > > I see.... > > The think is, I am interested to know if "e" is "Nothing", whatever the type > > of Nothing is! > > Data.Maybe.isNothing ? > > > > > > > > > On Wed, Jul 20, 2016 at 5:44 PM, Patrick Chilton > mailto:chpatrick@gmail.com mailto:chpatrick@gmail.com>> > > wrote: > >> > >> It's because you're doing === Nothing and the type of the Nothing is > >> ambiguous (Maybe a1). > >> > >> On Wed, Jul 20, 2016 at 5:18 PM, Corentin Dupont > >> mailto:corentin.dupont@gmail.com mailto:corentin.dupont@gmail.com>> wrote: > >>> > >>> Hi all, > >>> I'm surprised this doesn't work: > >>> > >>> data SomeData = forall e. (Typeable e, Eq e) => SomeData e > >>> > >>> (===) :: (Typeable a, Typeable b, Eq a, Eq b) => a -> b -> Bool > >>> (===) x y = cast x == Just y > >>> > >>> test :: SomeData' -> Bool > >>> test (SomeData' e) | e === Nothing = True > >>> test _ = False > >>> > >>> It says > >>> Could not deduce (Eq a1) arising from a use of ‘===’ > >>> > >>> How can I achieve something of the same effect? > >>> > >>> Thanks > >>> Corentin > >>> > >>> _______________________________________________ > >>> Haskell-Cafe mailing list > >>> To (un)subscribe, modify options or view archives go to: > >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe > >>> Only members subscribed via the mailman list are allowed to post. > >> > >> > > > > > > _______________________________________________ > > Haskell-Cafe mailing list > > To (un)subscribe, modify options or view archives go to: > > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe > > Only members subscribed via the mailman list are allowed to post. > > > > -- > Ivan Lazar Miljenovic > Ivan.Miljenovic@gmail.com mailto:Ivan.Miljenovic@gmail.com mailto:Ivan.Miljenovic@gmail.com> > http://IvanMiljenovic.wordpress.com > > > > > _______________________________________________ > Haskell-Cafe mailing list > To (un)subscribe, modify options or view archives go to: > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe > Only members subscribed via the mailman list are allowed to post. >

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Corentin Dupont

4:27 p.m.

That's great, it works, thanks. Now I am blocked on this one: data Foo a where A :: Foo a B :: Foo [a] deriving instance Typeable Foo deriving instance (Data a) => Data (Foo a) Could not deduce (a ~ [a0]) from the context (Typeable (Foo a), Data a) It would compile only if I comment the B constructor. How can I make a Data instance of Foo?? On Thu, Jul 21, 2016 at 11:26 AM, Jonas Scholl wrote:

...

With "just Typeable" I mean using only the Typeable class. As already mentioned by Michael, it is also possible to achieve the same effect with the Data class:

data SomeData = forall e. (Data e, Eq e) => SomeData e

isNothing'' :: SomeData -> Bool isNothing'' (SomeData a) = toConstr a == toConstr (Nothing :: Maybe ())

Depending on your use-case, this may be simpler and it avoids using unsafeCoerce, which may make one feel a little bit uneasy. On the other hand, it adds an additional constraint. Additionally, a programmer can write his own Data instance while Typeable instances are always generated by the compiler (in newer versions of GHC).

...
That's great, exactly what I need. What do you mean by "just Typeable"? Do you have another idea in mind?

On Thu, Jul 21, 2016 at 10:23 AM, Jonas Scholl mailto:anselm.scholl@tu-harburg.de> wrote:

If you want to use just Typeable, you can implement your own cast: Extract the TypeRep of the thing in SomeData, get the TyCon, which is the top-level constructor, i.e. Maybe without arguments, and compare it with the TyCon from Maybe. If they match, you coerce the value to Maybe () and use isNothing. While this is not completely safe, we do not evaluate the thing we just coerced to (), and thus are safe, as Maybe should have identical representation regardless of the type

On 07/21/2016 10:48 AM, Corentin Dupont wrote: parameter.

...
isNothing' :: SomeData -> Bool isNothing' (SomeData a) = tyCon == maybeTyCon && isNothing (unsafeCoerce a :: Maybe ()) where tyCon = typeRepTyCon (typeRep (mkProxy a)) maybeTyCon = typeRepTyCon $ typeRep (Proxy :: Proxy (Maybe

()))

...
mkProxy :: a -> Proxy a mkProxy = const Proxy

On 07/21/2016 09:51 AM, Corentin Dupont wrote: > Hi Ivan, > I could use isNothing, but the data is forall'ed... > I tried but it doesn't work: > > data SomeData = forall e. (Typeable e, Eq e) => SomeData e > > isNothing' :: SomeData -> Bool > isNothing' (SomeData a) = case (cast a) of > (a :: Maybe a) -> isNothing a > > Could not deduce (Typeable a) arising from a use of ‘cast’ > > On Wed, Jul 20, 2016 at 11:21 PM, Ivan Lazar Miljenovic > mailto:ivan.miljenovic@gmail.com mailto:ivan.miljenovic@gmail.com>> wrote: > > On 21 July 2016 at 02:30, Corentin Dupont <

corentin.dupont@gmail.com mailto:corentin.dupont@gmail.com

...
>
corentin.dupont@gmail.com>>> wrote:

...
> > I see.... > > The think is, I am interested to know if "e" is "Nothing",

whatever the type

...
> > of Nothing is! > > Data.Maybe.isNothing ? > > > > > > > > > On Wed, Jul 20, 2016 at 5:44 PM, Patrick Chilton > mailto:chpatrick@gmail.com mailto:chpatrick@gmail.com>> > > wrote: > >> > >> It's because you're doing === Nothing and the type of the

Nothing is

...
> >> ambiguous (Maybe a1). > >> > >> On Wed, Jul 20, 2016 at 5:18 PM, Corentin Dupont > >> mailto:corentin.dupont@gmail.com mailto:corentin.dupont@gmail.com>> wrote: > >>> > >>> Hi all, > >>> I'm surprised this doesn't work: > >>> > >>> data SomeData = forall e. (Typeable e, Eq e) => SomeData e > >>> > >>> (===) :: (Typeable a, Typeable b, Eq a, Eq b) => a -> b -> Bool > >>> (===) x y = cast x == Just y > >>> > >>> test :: SomeData' -> Bool > >>> test (SomeData' e) | e === Nothing = True > >>> test _ = False > >>> > >>> It says > >>> Could not deduce (Eq a1) arising from a use of ‘===’ > >>> > >>> How can I achieve something of the same effect? > >>> > >>> Thanks > >>> Corentin > >>> > >>> _______________________________________________ > >>> Haskell-Cafe mailing list > >>> To (un)subscribe, modify options or view archives go to: > >>>

http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

...
> >>> Only members subscribed via the mailman list are allowed to post. > >> > >> > > > > > > _______________________________________________ > > Haskell-Cafe mailing list > > To (un)subscribe, modify options or view archives go to: > >

http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

...
> > Only members subscribed via the mailman list are allowed to post. > > > > -- > Ivan Lazar Miljenovic > Ivan.Miljenovic@gmail.com mailto:Ivan.Miljenovic@gmail.com
...
> http://IvanMiljenovic.wordpress.com > > > > > _______________________________________________ > Haskell-Cafe mailing list > To (un)subscribe, modify options or view archives go to: > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe > Only members subscribed via the mailman list are allowed to post. >

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

David Feuer

22 Jul 22 Jul

5:45 a.m.

I would be surprised if GHC could derive a Data instance for a GADT. Deriving generally tends to fall down for GADTs. I also suspect Data doesn't work for GADTs at all. Generic mechanisms for GADTs in Haskell seem a bit researchy still. On Jul 21, 2016 4:27 PM, "Corentin Dupont" wrote:

...

That's great, it works, thanks. Now I am blocked on this one:

data Foo a where A :: Foo a B :: Foo [a]

deriving instance Typeable Foo deriving instance (Data a) => Data (Foo a)

Could not deduce (a ~ [a0]) from the context (Typeable (Foo a), Data a)

It would compile only if I comment the B constructor. How can I make a Data instance of Foo??

On Thu, Jul 21, 2016 at 11:26 AM, Jonas Scholl < anselm.scholl@tu-harburg.de> wrote:

...
With "just Typeable" I mean using only the Typeable class. As already mentioned by Michael, it is also possible to achieve the same effect with the Data class:

data SomeData = forall e. (Data e, Eq e) => SomeData e

isNothing'' :: SomeData -> Bool isNothing'' (SomeData a) = toConstr a == toConstr (Nothing :: Maybe ())

Depending on your use-case, this may be simpler and it avoids using unsafeCoerce, which may make one feel a little bit uneasy. On the other hand, it adds an additional constraint. Additionally, a programmer can write his own Data instance while Typeable instances are always generated by the compiler (in newer versions of GHC).

...
That's great, exactly what I need. What do you mean by "just Typeable"? Do you have another idea in mind?

On Thu, Jul 21, 2016 at 10:23 AM, Jonas Scholl mailto:anselm.scholl@tu-harburg.de> wrote:

If you want to use just Typeable, you can implement your own cast: Extract the TypeRep of the thing in SomeData, get the TyCon, which is the top-level constructor, i.e. Maybe without arguments, and compare it with the TyCon from Maybe. If they match, you coerce the value to Maybe () and use isNothing. While this is not completely safe, we do not evaluate the thing we just coerced to (), and thus are safe, as Maybe should have identical representation regardless of the type

On 07/21/2016 10:48 AM, Corentin Dupont wrote: parameter.

...
isNothing' :: SomeData -> Bool isNothing' (SomeData a) = tyCon == maybeTyCon && isNothing (unsafeCoerce a :: Maybe ()) where tyCon = typeRepTyCon (typeRep (mkProxy a)) maybeTyCon = typeRepTyCon $ typeRep (Proxy :: Proxy (Maybe

()))

...
mkProxy :: a -> Proxy a mkProxy = const Proxy

On 07/21/2016 09:51 AM, Corentin Dupont wrote: > Hi Ivan, > I could use isNothing, but the data is forall'ed... > I tried but it doesn't work: > > data SomeData = forall e. (Typeable e, Eq e) => SomeData e > > isNothing' :: SomeData -> Bool > isNothing' (SomeData a) = case (cast a) of > (a :: Maybe a) -> isNothing a > > Could not deduce (Typeable a) arising from a use of ‘cast’ > > On Wed, Jul 20, 2016 at 11:21 PM, Ivan Lazar Miljenovic > mailto:ivan.miljenovic@gmail.com mailto:ivan.miljenovic@gmail.com>> wrote: > > On 21 July 2016 at 02:30, Corentin Dupont <

corentin.dupont@gmail.com mailto:corentin.dupont@gmail.com

...
>
corentin.dupont@gmail.com>>> wrote:

...
> > I see.... > > The think is, I am interested to know if "e" is "Nothing",

whatever the type

...
> > of Nothing is! > > Data.Maybe.isNothing ? > > > > > > > > > On Wed, Jul 20, 2016 at 5:44 PM, Patrick Chilton > mailto:chpatrick@gmail.com mailto:chpatrick@gmail.com>> > > wrote: > >> > >> It's because you're doing === Nothing and the type of the

Nothing is

...
> >> ambiguous (Maybe a1). > >> > >> On Wed, Jul 20, 2016 at 5:18 PM, Corentin Dupont > >> mailto:corentin.dupont@gmail.com
corentin.dupont@gmail.com

...
mailto:corentin.dupont@gmail.com>> wrote: > >>> > >>> Hi all, > >>> I'm surprised this doesn't work: > >>> > >>> data SomeData = forall e. (Typeable e, Eq e) => SomeData e > >>> > >>> (===) :: (Typeable a, Typeable b, Eq a, Eq b) => a -> b -> Bool > >>> (===) x y = cast x == Just y > >>> > >>> test :: SomeData' -> Bool > >>> test (SomeData' e) | e === Nothing = True > >>> test _ = False > >>> > >>> It says > >>> Could not deduce (Eq a1) arising from a use of ‘===’ > >>> > >>> How can I achieve something of the same effect? > >>> > >>> Thanks > >>> Corentin > >>> > >>> _______________________________________________ > >>> Haskell-Cafe mailing list > >>> To (un)subscribe, modify options or view archives go to: > >>>

http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

...
> >>> Only members subscribed via the mailman list are allowed to post. > >> > >> > > > > > > _______________________________________________ > > Haskell-Cafe mailing list > > To (un)subscribe, modify options or view archives go to: > >

http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

...
> > Only members subscribed via the mailman list are allowed to post. > > > > -- > Ivan Lazar Miljenovic > Ivan.Miljenovic@gmail.com mailto:Ivan.Miljenovic@gmail.com
...
> http://IvanMiljenovic.wordpress.com > > > > > _______________________________________________ > Haskell-Cafe mailing list > To (un)subscribe, modify options or view archives go to: > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe > Only members subscribed via the mailman list are allowed to post. >

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Patrick Chilton

21 Jul 21 Jul

5:50 a.m.

You also might want to consider whether this existential approach is correct to begin with. Could you just use a Maybe SomeData instead? Do you need the existential at all? https://lukepalmer.wordpress.com/2010/01/24/haskell-antipattern-existential-... On Thu, Jul 21, 2016 at 10:48 AM, Corentin Dupont

...

wrote:

...

That's great, exactly what I need. What do you mean by "just Typeable"? Do you have another idea in mind?

On Thu, Jul 21, 2016 at 10:23 AM, Jonas Scholl < anselm.scholl@tu-harburg.de> wrote:

...
If you want to use just Typeable, you can implement your own cast: Extract the TypeRep of the thing in SomeData, get the TyCon, which is the top-level constructor, i.e. Maybe without arguments, and compare it with the TyCon from Maybe. If they match, you coerce the value to Maybe () and use isNothing. While this is not completely safe, we do not evaluate the thing we just coerced to (), and thus are safe, as Maybe should have identical representation regardless of the type parameter.

isNothing' :: SomeData -> Bool isNothing' (SomeData a) = tyCon == maybeTyCon && isNothing (unsafeCoerce a :: Maybe ()) where tyCon = typeRepTyCon (typeRep (mkProxy a)) maybeTyCon = typeRepTyCon $ typeRep (Proxy :: Proxy (Maybe ())) mkProxy :: a -> Proxy a mkProxy = const Proxy

...
Hi Ivan, I could use isNothing, but the data is forall'ed... I tried but it doesn't work:

data SomeData = forall e. (Typeable e, Eq e) => SomeData e

isNothing' :: SomeData -> Bool isNothing' (SomeData a) = case (cast a) of (a :: Maybe a) -> isNothing a

Could not deduce (Typeable a) arising from a use of ‘cast’

On Wed, Jul 20, 2016 at 11:21 PM, Ivan Lazar Miljenovic mailto:ivan.miljenovic@gmail.com> wrote:

On 21 July 2016 at 02:30, Corentin Dupont < corentin.dupont@gmail.com mailto:corentin.dupont@gmail.com> wrote: > I see.... > The think is, I am interested to know if "e" is "Nothing", whatever the type > of Nothing is!

Data.Maybe.isNothing ?

> > > > On Wed, Jul 20, 2016 at 5:44 PM, Patrick Chilton mailto:chpatrick@gmail.com> > wrote: >> >> It's because you're doing === Nothing and the type of the Nothing is >> ambiguous (Maybe a1). >> >> On Wed, Jul 20, 2016 at 5:18 PM, Corentin Dupont >> mailto:corentin.dupont@gmail.com> wrote: >>> >>> Hi all, >>> I'm surprised this doesn't work: >>> >>> data SomeData = forall e. (Typeable e, Eq e) => SomeData e >>> >>> (===) :: (Typeable a, Typeable b, Eq a, Eq b) => a -> b -> Bool >>> (===) x y = cast x == Just y >>> >>> test :: SomeData' -> Bool >>> test (SomeData' e) | e === Nothing = True >>> test _ = False >>> >>> It says >>> Could not deduce (Eq a1) arising from a use of ‘===’ >>> >>> How can I achieve something of the same effect? >>> >>> Thanks >>> Corentin >>> >>> _______________________________________________ >>> Haskell-Cafe mailing list >>> To (un)subscribe, modify options or view archives go to: >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe >>> Only members subscribed via the mailman list are allowed to

On 07/21/2016 09:51 AM, Corentin Dupont wrote: post.

...
>> >> > > > _______________________________________________ > Haskell-Cafe mailing list > To (un)subscribe, modify options or view archives go to: > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe > Only members subscribed via the mailman list are allowed to post.

-- Ivan Lazar Miljenovic Ivan.Miljenovic@gmail.com mailto:Ivan.Miljenovic@gmail.com http://IvanMiljenovic.wordpress.com

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Corentin Dupont

7:26 a.m.

That's right, there are hints that my design is overly complex, I'm looking at simplifying it. On Thu, Jul 21, 2016 at 11:50 AM, Patrick Chilton wrote:

...

You also might want to consider whether this existential approach is correct to begin with. Could you just use a Maybe SomeData instead? Do you need the existential at all? https://lukepalmer.wordpress.com/2010/01/24/haskell-antipattern-existential-...

On Thu, Jul 21, 2016 at 10:48 AM, Corentin Dupont < corentin.dupont@gmail.com> wrote:

...
That's great, exactly what I need. What do you mean by "just Typeable"? Do you have another idea in mind?

On Thu, Jul 21, 2016 at 10:23 AM, Jonas Scholl < anselm.scholl@tu-harburg.de> wrote:

...
If you want to use just Typeable, you can implement your own cast: Extract the TypeRep of the thing in SomeData, get the TyCon, which is the top-level constructor, i.e. Maybe without arguments, and compare it with the TyCon from Maybe. If they match, you coerce the value to Maybe () and use isNothing. While this is not completely safe, we do not evaluate the thing we just coerced to (), and thus are safe, as Maybe should have identical representation regardless of the type parameter.

isNothing' :: SomeData -> Bool isNothing' (SomeData a) = tyCon == maybeTyCon && isNothing (unsafeCoerce a :: Maybe ()) where tyCon = typeRepTyCon (typeRep (mkProxy a)) maybeTyCon = typeRepTyCon $ typeRep (Proxy :: Proxy (Maybe ())) mkProxy :: a -> Proxy a mkProxy = const Proxy

...
Hi Ivan, I could use isNothing, but the data is forall'ed... I tried but it doesn't work:

data SomeData = forall e. (Typeable e, Eq e) => SomeData e

isNothing' :: SomeData -> Bool isNothing' (SomeData a) = case (cast a) of (a :: Maybe a) -> isNothing a

Could not deduce (Typeable a) arising from a use of ‘cast’

On Wed, Jul 20, 2016 at 11:21 PM, Ivan Lazar Miljenovic mailto:ivan.miljenovic@gmail.com> wrote:

On 21 July 2016 at 02:30, Corentin Dupont < corentin.dupont@gmail.com mailto:corentin.dupont@gmail.com> wrote: > I see.... > The think is, I am interested to know if "e" is "Nothing", whatever the type > of Nothing is!

Data.Maybe.isNothing ?

> > > > On Wed, Jul 20, 2016 at 5:44 PM, Patrick Chilton mailto:chpatrick@gmail.com> > wrote: >> >> It's because you're doing === Nothing and the type of the Nothing is >> ambiguous (Maybe a1). >> >> On Wed, Jul 20, 2016 at 5:18 PM, Corentin Dupont >> mailto:corentin.dupont@gmail.com> wrote: >>> >>> Hi all, >>> I'm surprised this doesn't work: >>> >>> data SomeData = forall e. (Typeable e, Eq e) => SomeData e >>> >>> (===) :: (Typeable a, Typeable b, Eq a, Eq b) => a -> b -> Bool >>> (===) x y = cast x == Just y >>> >>> test :: SomeData' -> Bool >>> test (SomeData' e) | e === Nothing = True >>> test _ = False >>> >>> It says >>> Could not deduce (Eq a1) arising from a use of ‘===’ >>> >>> How can I achieve something of the same effect? >>> >>> Thanks >>> Corentin >>> >>> _______________________________________________ >>> Haskell-Cafe mailing list >>> To (un)subscribe, modify options or view archives go to: >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe >>> Only members subscribed via the mailman list are allowed to

On 07/21/2016 09:51 AM, Corentin Dupont wrote: post.

...
>> >> > > > _______________________________________________ > Haskell-Cafe mailing list > To (un)subscribe, modify options or view archives go to: > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe > Only members subscribed via the mailman list are allowed to post.

-- Ivan Lazar Miljenovic Ivan.Miljenovic@gmail.com mailto:Ivan.Miljenovic@gmail.com http://IvanMiljenovic.wordpress.com

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

3224

Age (days ago)

3226

Last active (days ago)

List overview

Download

12 comments

6 participants

participants (6)

Corentin Dupont
David Feuer
Ivan Lazar Miljenovic
Jonas Scholl
Michael Burge
Patrick Chilton