GHC.Generics: how to derive a Generic instance for an existential type?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

GHC.Generics: how to derive a Generic instance for an existential type?

Andreas Abel
I wonder whether GHC.Generics supports existential types yet...

{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE StandaloneDeriving #-}

import GHC.Generics

data U = forall a. (Generic a) => U a
   -- deriving (Generic)
     -- Can't make a derived instance of ‘Generic U’:
     --   Constructor ‘U’ has existentials or constraints in its type
     --   Possible fix: use a standalone deriving declaration instead

-- deriving instance Generic U
     -- Can't make a derived instance of ‘Generic U’:
     --   U must be a vanilla data constructor
     -- In the stand-alone deriving instance for ‘Generic U’

data D1Ser
data C1_0Ser

instance Generic U where
   type Rep U = D D1Ser (C1 C1_0Ser (S1 NoSelector (Rep a)))
     -- Not in scope: type variable ‘a’

-- How to bring the existential type `a' into scope?

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

[hidden email]
http://www2.tcs.ifi.lmu.de/~abel/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: GHC.Generics: how to derive a Generic instance for an existential type?

José Pedro Magalhães-3
Hi Andreas,

No, GHC.Generics doesn't support existentials.

If your existentials are used as arguments to constructors (like in the example you've provided), the only approach I'm aware of that might help you is this:

Alexey Rodriguez Yakushev and Johan Jeuring.
In Proceedings workshop on Approaches and Applications of Inductive Programming 2009.
(This reference seems to be missing its references. You could also look at Chapter 5 of Alexey's thesis.)

If your existentials are used only as indices, then you could look at this:

José Pedro Magalhães and Johan Jeuring.
In Proceedings of the 7th ACM SIGPLAN Workshop on Generic Programming (WGP'11), pp. 37–46, ACM, 2011.
(Chapter 10 of my thesis has a more up-to-date version.)


Cheers,
Pedro

On Sat, Jun 6, 2015 at 2:41 PM, Andreas Abel <[hidden email]> wrote:
I wonder whether GHC.Generics supports existential types yet...

{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE StandaloneDeriving #-}

import GHC.Generics

data U = forall a. (Generic a) => U a
  -- deriving (Generic)
    -- Can't make a derived instance of ‘Generic U’:
    --   Constructor ‘U’ has existentials or constraints in its type
    --   Possible fix: use a standalone deriving declaration instead

-- deriving instance Generic U
    -- Can't make a derived instance of ‘Generic U’:
    --   U must be a vanilla data constructor
    -- In the stand-alone deriving instance for ‘Generic U’

data D1Ser
data C1_0Ser

instance Generic U where
  type Rep U = D D1Ser (C1 C1_0Ser (S1 NoSelector (Rep a)))
    -- Not in scope: type variable ‘a’

-- How to bring the existential type `a' into scope?

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

[hidden email]
http://www2.tcs.ifi.lmu.de/~abel/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: GHC.Generics: how to derive a Generic instance for an existential type?

Andreas Abel-2
Dear Pedro,

thanks for the answer and your pointers to the literature.  As usual,
people want things to work *now*, and I am no exception. ;-)

It seems like generics are broken in ghc 7.6.3 which we support for
Agda, so I have to give up on generics for next years (until we drop
support for ghc < 7.8).

   https://code.google.com/p/agda/issues/detail?id=1558

Cheers,
Andreas

On 07.06.2015 09:34, José Pedro Magalhães wrote:

> Hi Andreas,
>
> No, GHC.Generics doesn't support existentials.
>
> If your existentials are used as arguments to constructors (like in the
> example you've provided), the only approach I'm aware of that might help
> you is this:
>
>     Alexey Rodriguez Yakushev and Johan Jeuring.
>     Enumerating Well-Typed Terms Generically.
>     <http://www.cs.uu.nl/research/techreps/UU-CS-2009-017.html>
>     In Proceedings workshop on Approaches and Applications of Inductive
>     Programming 2009.
>     (This reference seems to be missing its references. You could also
>     look at Chapter 5 of Alexey's thesis
>     <file:///C:/Users/Dreixel/Desktop/rodriguez.pdf>.)
>
>
> If your existentials are used only as indices, then you could look at this:
>
>     José Pedro Magalhães and Johan Jeuring.
>     Generic Programming for Indexed Datatypes.
>     <http://dreixel.net/research/pdf/gpid.pdf>
>     In Proceedings of the 7th ACM SIGPLAN Workshop on Generic
>     Programming (WGP'11), pp. 37–46, ACM, 2011.
>     (Chapter 10 of my thesis
>     <http://dreixel.net/index.php?content=thesis> has a more up-to-date
>     version.)
>
>
>
> Cheers,
> Pedro
>
> On Sat, Jun 6, 2015 at 2:41 PM, Andreas Abel <[hidden email]
> <mailto:[hidden email]>> wrote:
>
>     I wonder whether GHC.Generics supports existential types yet...
>
>     {-# LANGUAGE DeriveGeneric #-}
>     {-# LANGUAGE ExistentialQuantification #-}
>     {-# LANGUAGE StandaloneDeriving #-}
>
>     import GHC.Generics
>
>     data U = forall a. (Generic a) => U a
>        -- deriving (Generic)
>          -- Can't make a derived instance of ‘Generic U’:
>          --   Constructor ‘U’ has existentials or constraints in its type
>          --   Possible fix: use a standalone deriving declaration instead
>
>     -- deriving instance Generic U
>          -- Can't make a derived instance of ‘Generic U’:
>          --   U must be a vanilla data constructor
>          -- In the stand-alone deriving instance for ‘Generic U’
>
>     data D1Ser
>     data C1_0Ser
>
>     instance Generic U where
>        type Rep U = D D1Ser (C1 C1_0Ser (S1 NoSelector (Rep a)))
>          -- Not in scope: type variable ‘a’
>
>     -- How to bring the existential type `a' into scope?
>
>     --
>     Andreas Abel  <><      Du bist der geliebte Mensch.
>
>     Department of Computer Science and Engineering
>     Chalmers and Gothenburg University, Sweden
>
>     [hidden email] <mailto:[hidden email]>
>     http://www2.tcs.ifi.lmu.de/~abel/
>     _______________________________________________
>     Haskell-Cafe mailing list
>     [hidden email] <mailto:[hidden email]>
>     http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
>


--
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

[hidden email]
http://www2.tcs.ifi.lmu.de/~abel/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe