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,
21 -- a 'trans' being not necessarily injective nor surjective.
22 type BiTrans from to = (Trans from to, Trans to from)
24 -- ** Class 'Liftable'
25 -- | Convenient type class synonym for using 'Output'
26 type Liftable repr = Trans (Output repr) repr
27 lift :: forall repr a.
29 Output repr a -> repr a
30 lift = trans @(Output repr)
33 unlift :: forall repr a.
34 Trans repr (Output repr) =>
35 repr a -> Output repr a
39 -- ** Class 'Unliftable'
40 -- | Convenient type class synonym for using 'Output'
41 type Unliftable repr = Trans repr (Output repr)
44 class Trans1 from to where
52 trans1 f = trans . f . trans
55 -- ** Class 'Liftable1'
56 -- | Convenient type class synonym for using 'Output'
57 type Liftable1 repr = Trans1 (Output repr) repr
58 lift1 :: forall repr a b.
60 (Output repr a -> Output repr b) ->
62 lift1 = trans1 @(Output repr)
66 class Trans2 from to where
68 (from a -> from b -> from c) ->
72 (from a -> from b -> from c) ->
74 trans2 f a b = trans (f (trans a) (trans b))
77 -- ** Class 'Liftable2'
78 -- | Convenient type class synonym for using 'Output'
79 type Liftable2 repr = Trans2 (Output repr) repr
80 lift2 :: forall repr a b c.
82 (Output repr a -> Output repr b -> Output repr c) ->
83 repr a -> repr b -> repr c
84 lift2 = trans2 @(Output repr)
88 class Trans3 from to where
90 (from a -> from b -> from c -> from d) ->
91 to a -> to b -> to c -> to d
94 (from a -> from b -> from c -> from d) ->
95 to a -> to b -> to c -> to d
96 trans3 f a b c = trans (f (trans a) (trans b) (trans c))
99 -- ** Class 'Liftable3'
100 -- | Convenient type class synonym for using 'Output'
101 type Liftable3 repr = Trans3 (Output repr) repr
102 lift3 :: forall repr a b c d.
104 (Output repr a -> Output repr b -> Output repr c -> Output repr d) ->
105 repr a -> repr b -> repr c -> repr d
106 lift3 = trans3 @(Output repr)
110 -- | 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.
111 newtype Any repr a = Any { unAny :: repr a }
112 type instance Output (Any repr) = repr
113 instance Trans (Any repr) repr where
115 instance Trans1 (Any repr) repr
116 instance Trans2 (Any repr) repr
117 instance Trans3 (Any repr) repr
118 instance Trans repr (Any repr) where
120 instance Trans1 repr (Any repr)
121 instance Trans2 repr (Any repr)
122 instance Trans3 repr (Any repr)