Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
How to derive and use Generic instances for a subset of GADTs, using QuantifiedConstraints
{-# 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
You can’t perform that action at this time.