[Haskell-cafe] pattern match on forall'ed data

[Corentin Dupont]

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

[Patrick Chilton]

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

_______________________________________________
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]

I see....

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

[Michael Burge]

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.

[Ivan Lazar Miljenovic]

On 21 July 2016 at 02:30, Corentin Dupont <corenti...@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 ?

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

[Corentin Dupont]

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’

[Jonas Scholl]

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
> <ivan.mi...@gmail.com <mailto:ivan.mi...@gmail.com>> wrote:
>
> On 21 July 2016 at 02:30, Corentin Dupont <corenti...@gmail.com

> <mailto:corenti...@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

> <chpa...@gmail.com <mailto:chpa...@gmail.com>>

> Ivan.Mi...@gmail.com <mailto:Ivan.Mi...@gmail.com>
> http://IvanMiljenovic.wordpress.com

[Corentin Dupont]

That's great, exactly what I need.

What do you mean by "just Typeable"?

Do you have another idea in mind?

[Jonas Scholl]

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).

> <mailto:ivan.mi...@gmail.com

> <mailto:ivan.mi...@gmail.com>>> wrote:
> >
> > On 21 July 2016 at 02:30, Corentin Dupont <corenti...@gmail.com <mailto:corenti...@gmail.com>

> > <mailto:corenti...@gmail.com <mailto:corenti...@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
> > <chpa...@gmail.com <mailto:chpa...@gmail.com>

> <mailto:chpa...@gmail.com <mailto:chpa...@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
> > >> <corenti...@gmail.com

> <mailto:corenti...@gmail.com> <mailto:corenti...@gmail.com

> <mailto:Ivan.Mi...@gmail.com <mailto:Ivan.Mi...@gmail.com>>

[Patrick Chilton]

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-typeclass/

[Corentin Dupont]

That's right, there are hints that my design is overly complex, I'm looking at simplifying it.

[Corentin Dupont]

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??

[David Feuer]

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.