{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Comp.Multi.Projection (pr, (:<), (:*:)(..), ffst, fsnd) where
import Data.Comp.SubsumeCommon
import Data.Comp.Multi.Ops hiding (Elem)
import Data.Kind
type family Elem (f :: Type -> Type)
(g :: Type -> Type) :: Emb where
Elem f f = Found Here
Elem (f1 :*: f2) g = Sum' (Elem f1 g) (Elem f2 g)
Elem f (g1 :*: g2) = Choose (Elem f g1) (Elem f g2)
Elem f g = NotFound
class Proj (e :: Emb) (p :: Type -> Type)
(q :: Type -> Type) where
pr' :: Proxy e -> q a -> p a
instance Proj (Found Here) f f where
pr' :: forall a. Proxy ('Found 'Here) -> f a -> f a
pr' Proxy ('Found 'Here)
_ = forall a. a -> a
id
instance Proj (Found p) f g => Proj (Found (Le p)) f (g :*: g') where
pr' :: forall a. Proxy ('Found ('Le p)) -> (:*:) g g' a -> f a
pr' Proxy ('Found ('Le p))
_ = forall (e :: Emb) (p :: * -> *) (q :: * -> *) a.
Proj e p q =>
Proxy e -> q a -> p a
pr' (forall {k} (a :: k). Proxy a
P :: Proxy (Found p)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (g :: k -> *) (a :: k). (:*:) f g a -> f a
ffst
instance Proj (Found p) f g => Proj (Found (Ri p)) f (g' :*: g) where
pr' :: forall a. Proxy ('Found ('Ri p)) -> (:*:) g' g a -> f a
pr' Proxy ('Found ('Ri p))
_ = forall (e :: Emb) (p :: * -> *) (q :: * -> *) a.
Proj e p q =>
Proxy e -> q a -> p a
pr' (forall {k} (a :: k). Proxy a
P :: Proxy (Found p)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (g :: k -> *) (a :: k). (:*:) f g a -> g a
fsnd
instance (Proj (Found p1) f1 g, Proj (Found p2) f2 g)
=> Proj (Found (Sum p1 p2)) (f1 :*: f2) g where
pr' :: forall a. Proxy ('Found ('Sum p1 p2)) -> g a -> (:*:) f1 f2 a
pr' Proxy ('Found ('Sum p1 p2))
_ g a
x = (forall (e :: Emb) (p :: * -> *) (q :: * -> *) a.
Proj e p q =>
Proxy e -> q a -> p a
pr' (forall {k} (a :: k). Proxy a
P :: Proxy (Found p1)) g a
x forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> (:*:) f g a
:*: forall (e :: Emb) (p :: * -> *) (q :: * -> *) a.
Proj e p q =>
Proxy e -> q a -> p a
pr' (forall {k} (a :: k). Proxy a
P :: Proxy (Found p2)) g a
x)
infixl 5 :<
type f :< g = (Proj (ComprEmb (Elem f g)) f g)
pr :: forall p q a . (p :< q) => q a -> p a
pr :: forall (p :: * -> *) (q :: * -> *) a. (p :< q) => q a -> p a
pr = forall (e :: Emb) (p :: * -> *) (q :: * -> *) a.
Proj e p q =>
Proxy e -> q a -> p a
pr' (forall {k} (a :: k). Proxy a
P :: Proxy (ComprEmb (Elem p q)))