Last active
July 10, 2018 13:13
-
-
Save RyanGlScott/71d9f933e823b4a03f99de54d4b94d51 to your computer and use it in GitHub Desktop.
How to derive and use Generic instances for a subset of GADTs, using QuantifiedConstraints
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE ConstraintKinds #-} | |
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE FlexibleContexts #-} | |
{-# LANGUAGE GADTs #-} | |
{-# LANGUAGE KindSignatures #-} | |
{-# LANGUAGE QuantifiedConstraints #-} | |
{-# LANGUAGE RankNTypes #-} | |
{-# LANGUAGE ScopedTypeVariables #-} | |
{-# LANGUAGE TypeFamilies #-} | |
{-# LANGUAGE TypeOperators #-} | |
{-# LANGUAGE UndecidableInstances #-} | |
module GenericForSomeGADTs where | |
import Data.Kind | |
import GHC.Generics | |
----- | |
-- The ECC (Existential Constructor Context) type | |
----- | |
data ECC :: Constraint -> (Type -> Type) -> Type -> Type where | |
ECC :: c => { unECC :: f a } -> ECC c f a | |
instance (c => Eq (f a)) => Eq (ECC c f a) where | |
ECC x == ECC y = (x == y) | |
----- | |
-- An example Generic instance using ECC | |
----- | |
data MyGADT :: Type -> Type where | |
MyGADT1 :: Int -> MyGADT Int | |
MyGADT2 :: Eq a => a -> MyGADT a | |
MyGADT3 :: (a ~ Bool) => a -> MyGADT a | |
MyGADT4 :: MyGADT Bool -> MyGADT Bool | |
instance Generic (MyGADT a) where | |
type Rep (MyGADT a) = | |
D1 (MetaData "MyGADT" "GenericForSomeGADTs" "future-haskell" False) | |
( C1 (MetaCons "MyGADT1" PrefixI False) | |
(ECC (a ~ Int) | |
(S1 (MetaSel Nothing NoSourceUnpackedness NoSourceStrictness DecidedLazy) | |
(Rec0 Int))) | |
:+: C1 (MetaCons "MyGADT2" PrefixI False) | |
(ECC (Eq a) | |
(S1 (MetaSel Nothing NoSourceUnpackedness NoSourceStrictness DecidedLazy) | |
(Rec0 a))) | |
:+: C1 (MetaCons "MyGADT3" PrefixI False) | |
(ECC (a ~ Bool) | |
(S1 (MetaSel Nothing NoSourceUnpackedness NoSourceStrictness DecidedLazy) | |
(Rec0 a))) | |
:+: C1 (MetaCons "MyGADT4" PrefixI False) | |
(ECC (a ~ Bool) | |
(S1 (MetaSel Nothing NoSourceUnpackedness NoSourceStrictness DecidedLazy) | |
(Rec0 (MyGADT Bool)))) | |
) | |
from (MyGADT1 x) = M1 (L1 (M1 (ECC (M1 (K1 x))))) | |
from (MyGADT2 x) = M1 (R1 (L1 (M1 (ECC (M1 (K1 x)))))) | |
from (MyGADT3 x) = M1 (R1 (R1 (L1 (M1 (ECC (M1 (K1 x))))))) | |
from (MyGADT4 x) = M1 (R1 (R1 (R1 (M1 (ECC (M1 (K1 x))))))) | |
to (M1 (L1 (M1 (ECC (M1 (K1 x)))))) = MyGADT1 x | |
to (M1 (R1 (L1 (M1 (ECC (M1 (K1 x))))))) = MyGADT2 x | |
to (M1 (R1 (R1 (L1 (M1 (ECC (M1 (K1 x)))))))) = MyGADT3 x | |
to (M1 (R1 (R1 (R1 (M1 (ECC (M1 (K1 x)))))))) = MyGADT4 x | |
----- | |
-- How to use it | |
----- | |
genericEq :: forall a. (Generic a, Eq (Rep a ())) => a -> a -> Bool | |
genericEq x y = from' x == from' y | |
where | |
from' :: a -> Rep a () | |
from' = from | |
instance Eq (MyGADT a) where | |
(==) = genericEq | |
----- | |
-- The RFC (Rank-n Field Context) type | |
----- | |
newtype RFC :: Constraint -> (Type -> Type) -> Type -> Type where | |
RFC :: { unRFC :: c => f a } -> RFC c f a | |
instance (c => Functor f) => Functor (RFC c f) where | |
fmap f (RFC x) = RFC (fmap f x) | |
newtype RankNExample f a = RankNExample (Functor f => f a) | |
instance Generic1 (RankNExample f) where | |
type Rep1 (RankNExample f) = | |
D1 (MetaData "RankNExample" "GenericForSomeGADTs" "future-haskell" True) | |
(C1 (MetaCons "RankNExample" PrefixI False) | |
(S1 (MetaSel Nothing NoSourceUnpackedness NoSourceStrictness DecidedLazy) | |
(RFC (Functor f) | |
(Rec1 f)))) | |
from1 (RankNExample x) = M1 (M1 (M1 (RFC (Rec1 x)))) | |
to1 (M1 (M1 (M1 (RFC x)))) = RankNExample (unRec1 x) | |
----- | |
-- How to use it | |
----- | |
genericFmap :: (Generic1 f, Functor (Rep1 f)) => (a -> b) -> f a -> f b | |
genericFmap f = to1 . fmap f . from1 | |
instance Functor (RankNExample f) where | |
fmap = genericFmap |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment