Skip to content

Instantly share code, notes, and snippets.

Forked from Lysxia/Foo.hs
Created May 10, 2020 02:57
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save dmjio/66c49c62923b76d91c772d78bab93597 to your computer and use it in GitHub Desktop.
UndecidableInstances #-}
import Data.Kind (Type)
import Data.Coerce
import GHC.Generics
-- Example
data Foo
= Foo1
| Foo2 Foo
| Foo3 Foo Foo
deriving Generic
data T3 a b c = T3 a b c
deriving Generic
foo1 :: _
foo2 :: _
foo3 :: _
(T3 foo1 foo2 foo3) = magic @Foo @(T3 _ _ _)
example :: [Foo]
example = [foo1, foo2 Foo1, foo3 Foo1 Foo1]
-- Implementation
type family Productify (a :: Type) (f :: Type -> Type) :: Type -> Type where
Productify a (M1 D c f) = M1 D c (Productify a f)
Productify a (f :+: g) = Productify a f :*: Productify a g
Productify a (M1 C c f) = M1 S c (K1 R (Arrowify f a))
type family Arrowify (f :: Type -> Type) (a :: Type) :: Type where
Arrowify (f :*: g) a = Arrowify f (Arrowify g a)
Arrowify U1 a = a
Arrowify (M1 S c (K1 i t)) a = t -> a
class GProductify f where
gproductify :: (f p -> a) -> Productify a f p
instance GProductify f => GProductify (M1 D c f) where
gproductify f = M1 (gproductify (f . M1))
instance (GProductify f, GProductify g) => GProductify (f :+: g) where
gproductify f = gproductify (f . L1) :*: gproductify (f . R1)
instance GArrowify f => GProductify (M1 C c f) where
gproductify f = M1 (K1 (garrowify (f . M1)))
class GArrowify f where
garrowify :: (f p -> a) -> Arrowify f a
instance (GArrowify f, GArrowify g) => GArrowify (f :*: g) where
garrowify f = garrowify (\x -> garrowify (\y -> f (x :*: y)))
instance GArrowify (M1 S c (K1 i t)) where
garrowify = coerce
instance GArrowify U1 where
garrowify f = f U1
type family Fields (f :: Type -> Type) :: Type where
Fields (M1 i c f) = Fields f
Fields (f :*: g) = (Fields f, Fields g)
Fields (K1 i a) = a
productify_ :: forall a p. (Generic a, GProductify (Rep a)) => Productify a (Rep a) ()
productify_ = gproductify @(Rep a) @() @a (to @a)
magic :: forall a b.
( Generic a, GProductify (Rep a)
, Generic b, Coercible (Productify a (Rep a)) (Rep b), Fields (Productify a (Rep a)) ~ Fields (Rep b)) =>
magic = to (coerce' (productify_ @a @())) where
coerce' :: Productify a (Rep a) () -> Rep b ()
coerce' = coerce
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment