1 {-# LANGUAGE ConstraintKinds #-} -- For type class synonyms
2 {-# LANGUAGE DefaultSignatures #-} -- For adding Trans* constraints
3 module Symantic.Univariant.Trans where
5 -- TODO: move to symantic-univariant
7 import Data.Function ((.))
8 import Data.Kind (Type)
10 -- * Type family 'Output'
11 type family Output (repr :: Type -> Type) :: Type -> Type
14 -- | A 'trans'lation from an interpreter @(from)@ to an interpreter @(to)@.
15 class Trans from to where
16 trans :: from a -> to a
19 -- | Convenient type class synonym.
20 -- Note that this is not necessarily a bijective 'trans'lation, a 'trans' being not necessarily injective nor surjective.
21 type BiTrans from to = (Trans from to, Trans to from)
23 -- ** Class 'Liftable'
24 -- | Convenient type class synonym for using 'Output'
25 type Liftable repr = Trans (Output repr) repr
26 lift :: forall repr a.
28 Output repr a -> repr a
29 lift = trans @(Output repr)
32 unlift :: forall repr a.
33 Trans repr (Output repr) =>
34 repr a -> Output repr a
38 -- ** Class 'Unliftable'
39 -- | Convenient type class synonym for using 'Output'
40 type Unliftable repr = Trans repr (Output repr)
43 class Trans1 from to where
51 trans1 f = trans . f . trans
54 -- ** Class 'Liftable1'
55 -- | Convenient type class synonym for using 'Output'
56 type Liftable1 repr = Trans1 (Output repr) repr
57 lift1 :: forall repr a b.
59 (Output repr a -> Output repr b) ->
61 lift1 = trans1 @(Output repr)
65 class Trans2 from to where
67 (from a -> from b -> from c) ->
71 (from a -> from b -> from c) ->
73 trans2 f a b = trans (f (trans a) (trans b))
76 -- ** Class 'Liftable2'
77 -- | Convenient type class synonym for using 'Output'
78 type Liftable2 repr = Trans2 (Output repr) repr
79 lift2 :: forall repr a b c.
81 (Output repr a -> Output repr b -> Output repr c) ->
82 repr a -> repr b -> repr c
83 lift2 = trans2 @(Output repr)
87 class Trans3 from to where
89 (from a -> from b -> from c -> from d) ->
90 to a -> to b -> to c -> to d
93 (from a -> from b -> from c -> from d) ->
94 to a -> to b -> to c -> to d
95 trans3 f a b c = trans (f (trans a) (trans b) (trans c))
98 -- ** Class 'Liftable3'
99 -- | Convenient type class synonym for using 'Output'
100 type Liftable3 repr = Trans3 (Output repr) repr
101 lift3 :: forall repr a b c d.
103 (Output repr a -> Output repr b -> Output repr c -> Output repr d) ->
104 repr a -> repr b -> repr c -> repr d
105 lift3 = trans3 @(Output repr)
109 -- | A newtype to disambiguate the 'Trans' instance to any other interpreter when there is also one or more 'Trans's to other interpreters with a different interpretation than the generic one.
110 newtype Any repr a = Any { unAny :: repr a }
111 type instance Output (Any repr) = repr
112 instance Trans (Any repr) repr where
114 instance Trans1 (Any repr) repr
115 instance Trans2 (Any repr) repr
116 instance Trans3 (Any repr) repr
117 instance Trans repr (Any repr) where
119 instance Trans1 repr (Any repr)
120 instance Trans2 repr (Any repr)
121 instance Trans3 repr (Any repr)