module Hask.Rel where
import Hask.Core
type family Rel :: i -> j
type instance Rel = Const1
type instance Rel = Const2
type instance Rel = ConstC
type instance Rel = Id0
type instance Rel = Id1
type instance Rel = IdC
type instance Rel = Dict
type instance Rel = No
type family Reflected :: j -> i
type instance Reflected = Colim1
type instance Reflected = Colim2
type instance Reflected = Id0
type instance Reflected = Id1
type instance Reflected = IdC
type family Coreflected :: j -> i
type instance Coreflected = Lim1
type instance Coreflected = Lim2
type instance Coreflected = LimC
type instance Coreflected = Id0
type instance Coreflected = Id1
type instance Coreflected = IdC
class (f :: j -> i) ~| (u :: i -> k) | f k -> u, u j -> f where
radj :: Iso (f a ~> b) (f a' ~> b') (Rel a ~> u b) (Rel a' ~> u b')
instance Id0 ~| Id0 where radj = adj.pre _Id
instance Id1 ~| Id1 where radj = adj.pre _Id
instance IdC ~| IdC where radj = adj.pre _Id
instance Const1 ~| Lim1 where radj = adj.pre _Id
instance Const2 ~| Lim2 where radj = adj.pre _Id
instance ConstC ~| LimC where radj = adj.pre _Id
instance (Colim1 :: (i -> *) -> *) ~| (Const1 :: * -> i -> *) where radj = adj.pre _Id
class Functor m => RelMonad (m :: j -> c) where
runit :: Rel a ~> m a
rbind :: (Rel a ~> m b) -> m a ~> m b
instance RelMonad Id1 where
runit = id
rbind = id
instance RelMonad IdC where
runit = id
rbind = id
instance RelMonad Const1 where
runit = id
rbind = id
instance RelMonad Const2 where
runit = id
rbind = id
instance RelMonad ConstC where
runit = id
rbind = id
class (rel ~ Rel, Tensor (RelCompose :: (j -> c) -> (j -> c) -> j -> c)) => RelComposed (rel :: j -> c) where
type RelCompose :: (j -> c) -> (j -> c) -> (j -> c)
rcomposed :: Functor f' =>
Iso (RelCompose f) (RelCompose f')
(Compose (Lan rel f)) (Compose (Lan rel f'))
instance RelComposed Id0 where
type RelCompose = Compose1
rcomposed = mapping (un epsilonLan)
instance RelComposed Id1 where
type RelCompose = Compose2
rcomposed = mapping (un epsilonLan)
newtype ComposeConst1 (f :: * -> i -> *) (g :: * -> i -> *) (a :: *) (b :: i) = ComposeConst1 { decomposeConst1 :: Compose2 (Lan2 Const1 f) g a b }
instance Functor ComposeConst1 where
fmap f = Nat $ dimap (nat2 decomposeConst1) (nat2 ComposeConst1) $ first $ fmap1 f
instance Functor (ComposeConst1 f) where
fmap f = dimap (nat2 decomposeConst1) (nat2 ComposeConst1) $ Nat $ composed $ fmap2 $ runNat f
instance Functor g => Functor (ComposeConst1 f g) where
fmap f = dimap (Nat decomposeConst1) (Nat ComposeConst1) $ composed $ fmap2 $ fmap f
instance Semitensor ComposeConst1 where
type Tensorable ComposeConst1 = Functor
second f = runNat (beget rcomposed) . Nat (composed (fmap2 (runNat f))) . runNat (get rcomposed)
associate = dimap (runNat (beget rcomposed) . Nat (composed go) . runNat (get rcomposed)) undefined where
go :: Lan2 Const1 (ComposeConst1 a b) (c x) ~> Lan2 Const1 a (ComposeConst1 b c x)
go = Nat $ \(Lan2 l) -> Lan2 $ \a2zc -> undefined
type instance I ComposeConst1 = Const1
instance Tensor ComposeConst1 where
lambda = undefined
rho = dimap (nat2 $ undefined . runNat decompose . decomposeConst1)
(nat2 $ \a -> ComposeConst1 $ runNat compose $ Lan2 $ \k -> runNat decompose $ runNat2 k a)
instance RelComposed Const1 where
type RelCompose = ComposeConst1
rcomposed = dimap (nat3 decomposeConst1) (nat3 ComposeConst1)