Last active
March 2, 2020 02:07
Star
You must be signed in to star a gist
Generic (co)products
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 LambdaCase, EmptyCase, AllowAmbiguousTypes #-} | |
module SOP.Products where | |
import MyPrelude | |
import GHC.Generics | |
import Data.Void | |
import Data.Proxy | |
import Optics | |
type family TProduct (xs :: [*]) :: * | |
where | |
TProduct '[] = () | |
TProduct (x ': xs) = (x, TProduct xs) | |
class Append (xs :: [*]) (ys :: [*]) (zs :: [*]) | xs ys -> zs | |
where | |
(&&&) :: Proxy xs -> Proxy ys -> Iso' (TProduct xs, TProduct ys) (TProduct zs) | |
instance Append '[] ys ys | |
where | |
_ &&& _ = iso snd ((),) | |
instance Append xs ys zs => Append (x ': xs) ys (x ': zs) | |
where | |
(_ :: Proxy (x ': xs)) &&& (_ :: Proxy ys) = iso | |
(\((x, xs), ys) -> (x, fwd (Proxy @xs &&& Proxy @ys) (xs, ys))) | |
(\(x, zs) -> let (xs, ys) = bwd (Proxy @xs &&& Proxy @ys) zs in ((x, xs), ys)) | |
class Product c xs | c -> xs | |
where | |
asProduct :: Iso' c (TProduct xs) | |
instance Product (V1 p) '[Void] | |
where | |
asProduct = iso (\case {}) (absurd . fst) | |
instance Product (U1 p) '[] | |
where | |
asProduct = iso (const ()) (const U1) | |
instance Product (K1 i c p) '[c] | |
where | |
asProduct = iso (\(K1 c) -> (c, ())) (\(c, _) -> K1 c) | |
instance Product (f p) xs => Product (M1 i c f p) xs | |
where | |
asProduct = iso (\(M1 fp) -> fwd asProduct fp) (M1 . bwd asProduct) | |
instance (Product (f p) xs, Product (g p) ys, Append xs ys zs) => Product ((f :*: g) p) zs | |
where | |
asProduct = iso | |
(\(fp :*: gp) -> fwd (Proxy @xs &&& Proxy @ys) $ (fwd asProduct fp, fwd asProduct gp)) | |
((\(xs, ys) -> bwd asProduct xs :*: bwd asProduct ys) . bwd (Proxy @xs &&& Proxy @ys)) | |
gprod :: forall a x xs. (Generic a, Product (Rep a x) xs) => Iso' a (TProduct xs) | |
gprod = iso from to . asProduct @(Rep a x) @xs |
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 TypeFamilies, FunctionalDependencies, LambdaCase, AllowAmbiguousTypes #-} | |
module SOP.Sums where | |
import MyPrelude | |
import GHC.Generics | |
import Data.Proxy | |
import Data.Void | |
import Data.Bifunctor (Bifunctor(..)) | |
import Optics | |
type family Sum (xs :: [*]) :: * | |
where | |
Sum '[] = Void | |
Sum (x ': xs) = Either x (Sum xs) | |
class Coproduct c xs | c -> xs | |
where | |
asCoproduct :: Iso' c (Sum xs) | |
instance Coproduct (U1 p) '[()] | |
where | |
asCoproduct = iso (\U1 -> Left ()) (either (const U1) absurd) | |
instance Coproduct (K1 i c p) '[c] | |
where | |
asCoproduct = iso (\(K1 c) -> Left c) (either K1 absurd) | |
instance (Functor f, Coproduct (f p) xs) => Coproduct (M1 i c f p) xs | |
where | |
asCoproduct = iso (\(M1 fp) -> fwd asCoproduct fp) (M1 . bwd asCoproduct) | |
class Append (xs :: [*]) (ys :: [*]) (zs :: [*]) | xs ys -> zs | |
where | |
(|||) :: Proxy xs -> Proxy ys -> Iso' (Either (Sum xs) (Sum ys)) (Sum zs) | |
instance Append '[] ys ys | |
where | |
_ ||| _ = iso (either absurd id) Right | |
instance Append xs ys zs => Append (x ': xs) ys (x ': zs) | |
where | |
(_ :: Proxy (x ': xs)) ||| (_ :: Proxy ys) = iso | |
(either | |
(either Left (Right . fwd (Proxy @xs ||| Proxy @ys) . Left)) | |
(Right . fwd (Proxy @xs ||| Proxy @ys) . Right)) | |
(either (Left . Left) (first Right . bwd (Proxy @xs ||| Proxy @ys))) | |
instance (Coproduct (f p) xs, Coproduct (g p) ys, Append xs ys zs) => Coproduct ((f :+: g) p) zs | |
where | |
asCoproduct = iso | |
(\case | |
{ L1 fp -> fwd (Proxy @xs ||| Proxy @ys) $ Left $ fwd asCoproduct fp | |
; R1 gp -> fwd (Proxy @xs ||| Proxy @ys) $ Right $ fwd asCoproduct gp | |
}) | |
(either (L1 . bwd asCoproduct) (R1 . bwd asCoproduct) . bwd (Proxy @xs ||| Proxy @ys)) | |
-- TODO: @lysxia suggested that this can be done better using a CPS approach here https://funprog.zulipchat.com/#narrow/stream/201385-Haskell/topic/Illegal.20type.20synonym.20family.20in.20instance/near/189455360 | |
-- try that out | |
gcoprod :: forall a x xs. (Generic a, Coproduct (Rep a x) xs) => Iso' a (Sum xs) | |
gcoprod = iso from to . asCoproduct @(Rep a x) @xs |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment