{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DefaultSignatures #-}
module Symantic.Univariant.Trans where
import Data.Function ((.))
import Data.Kind (Type)
type family Output (repr :: Type -> Type) :: Type -> Type
class Trans from to where
trans :: from a -> to a
type BiTrans from to = (Trans from to, Trans to from)
type Liftable repr = Trans (Output repr) repr
lift :: forall repr a.
Liftable repr =>
Output repr a -> repr a
lift :: forall (repr :: * -> *) a. Liftable repr => Output repr a -> repr a
lift = forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans @(Output repr)
{-# INLINE lift #-}
unlift :: forall repr a.
Trans repr (Output repr) =>
repr a -> Output repr a
unlift :: forall (repr :: * -> *) a.
Trans repr (Output repr) =>
repr a -> Output repr a
unlift = forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans @repr
{-# INLINE unlift #-}
type Unliftable repr = Trans repr (Output repr)
class Trans1 from to where
trans1 ::
(from a -> from b) ->
to a -> to b
default trans1 ::
BiTrans from to =>
(from a -> from b) ->
to a -> to b
trans1 from a -> from b
f = from b -> to b
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans (from b -> to b) -> (to a -> from b) -> to a -> to b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. from a -> from b
f (from a -> from b) -> (to a -> from a) -> to a -> from b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. to a -> from a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans
{-# INLINE trans1 #-}
type Liftable1 repr = Trans1 (Output repr) repr
lift1 :: forall repr a b.
Liftable1 repr =>
(Output repr a -> Output repr b) ->
repr a -> repr b
lift1 :: forall (repr :: * -> *) a b.
Liftable1 repr =>
(Output repr a -> Output repr b) -> repr a -> repr b
lift1 = forall (from :: * -> *) (to :: * -> *) a b.
Trans1 from to =>
(from a -> from b) -> to a -> to b
trans1 @(Output repr)
{-# INLINE lift1 #-}
class Trans2 from to where
trans2 ::
(from a -> from b -> from c) ->
to a -> to b -> to c
default trans2 ::
BiTrans from to =>
(from a -> from b -> from c) ->
to a -> to b -> to c
trans2 from a -> from b -> from c
f to a
a to b
b = from c -> to c
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans (from a -> from b -> from c
f (to a -> from a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans to a
a) (to b -> from b
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans to b
b))
{-# INLINE trans2 #-}
type Liftable2 repr = Trans2 (Output repr) repr
lift2 :: forall repr a b c.
Liftable2 repr =>
(Output repr a -> Output repr b -> Output repr c) ->
repr a -> repr b -> repr c
lift2 :: forall (repr :: * -> *) a b c.
Liftable2 repr =>
(Output repr a -> Output repr b -> Output repr c)
-> repr a -> repr b -> repr c
lift2 = forall (from :: * -> *) (to :: * -> *) a b c.
Trans2 from to =>
(from a -> from b -> from c) -> to a -> to b -> to c
trans2 @(Output repr)
{-# INLINE lift2 #-}
class Trans3 from to where
trans3 ::
(from a -> from b -> from c -> from d) ->
to a -> to b -> to c -> to d
default trans3 ::
BiTrans from to =>
(from a -> from b -> from c -> from d) ->
to a -> to b -> to c -> to d
trans3 from a -> from b -> from c -> from d
f to a
a to b
b to c
c = from d -> to d
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans (from a -> from b -> from c -> from d
f (to a -> from a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans to a
a) (to b -> from b
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans to b
b) (to c -> from c
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans to c
c))
{-# INLINE trans3 #-}
type Liftable3 repr = Trans3 (Output repr) repr
lift3 :: forall repr a b c d.
Liftable3 repr =>
(Output repr a -> Output repr b -> Output repr c -> Output repr d) ->
repr a -> repr b -> repr c -> repr d
lift3 :: forall (repr :: * -> *) a b c d.
Liftable3 repr =>
(Output repr a -> Output repr b -> Output repr c -> Output repr d)
-> repr a -> repr b -> repr c -> repr d
lift3 = forall (from :: * -> *) (to :: * -> *) a b c d.
Trans3 from to =>
(from a -> from b -> from c -> from d)
-> to a -> to b -> to c -> to d
trans3 @(Output repr)
{-# INLINE lift3 #-}
newtype Any repr a = Any { forall (repr :: * -> *) a. Any repr a -> repr a
unAny :: repr a }
type instance Output (Any repr) = repr
instance Trans (Any repr) repr where
trans :: forall a. Any repr a -> repr a
trans = Any repr a -> repr a
forall (repr :: * -> *) a. Any repr a -> repr a
unAny
instance Trans1 (Any repr) repr
instance Trans2 (Any repr) repr
instance Trans3 (Any repr) repr
instance Trans repr (Any repr) where
trans :: forall a. repr a -> Any repr a
trans = repr a -> Any repr a
forall (repr :: * -> *) a. repr a -> Any repr a
Any
instance Trans1 repr (Any repr)
instance Trans2 repr (Any repr)
instance Trans3 repr (Any repr)