]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Type/Tuple.hs
factorizing Type1_From ast Type0
[haskell/symantic.git] / Language / Symantic / Type / Tuple.hs
1 {-# LANGUAGE FlexibleContexts #-}
2 {-# LANGUAGE FlexibleInstances #-}
3 {-# LANGUAGE MultiParamTypeClasses #-}
4 {-# LANGUAGE PatternSynonyms #-}
5 {-# LANGUAGE ScopedTypeVariables #-}
6 {-# LANGUAGE TypeFamilies #-}
7 {-# OPTIONS_GHC -fno-warn-orphans #-}
8 module Language.Symantic.Type.Tuple where
9
10 import qualified Data.MonoTraversable as MT
11 import Data.Proxy
12 import Data.Type.Equality ((:~:)(Refl))
13
14 import Language.Symantic.Type.Root
15 import Language.Symantic.Type.Type0
16 import Language.Symantic.Type.Type1
17 import Language.Symantic.Type.Type2
18 import Language.Symantic.Type.Constraint
19 import Language.Symantic.Type.Family
20
21 -- * Type 'Type_Tuple2'
22 -- | The @(,)@ type.
23 type Type_Tuple2 = Type2 (Proxy (,))
24
25 pattern Type_Tuple2
26 :: root a -> root b
27 -> Type_Tuple2 root ((,) a b)
28 pattern Type_Tuple2 a b
29 = Type2 Proxy a b
30
31 instance Type1_Unlift Type_Tuple2 where
32 type1_unlift (Type2 px a b) k =
33 k ( Type1 (Proxy::Proxy ((,) a)) b
34 , Type1_Lift (\(Type1 _ b') -> Type2 px a b')
35 )
36 instance
37 Type0_Constraint Eq root =>
38 Type0_Constraint Eq (Type_Tuple2 root) where
39 type0_constraint c (Type2 _ a b)
40 | Just Dict <- type0_constraint c a
41 , Just Dict <- type0_constraint c b
42 = Just Dict
43 type0_constraint _c _ = Nothing
44 instance
45 Type0_Constraint Ord root =>
46 Type0_Constraint Ord (Type_Tuple2 root) where
47 type0_constraint c (Type2 _ a b)
48 | Just Dict <- type0_constraint c a
49 , Just Dict <- type0_constraint c b
50 = Just Dict
51 type0_constraint _c _ = Nothing
52 instance
53 Type0_Constraint Monoid root =>
54 Type0_Constraint Monoid (Type_Tuple2 root) where
55 type0_constraint c (Type2 _ a b)
56 | Just Dict <- type0_constraint c a
57 , Just Dict <- type0_constraint c b
58 = Just Dict
59 type0_constraint _c _ = Nothing
60 instance Type0_Constraint Num (Type_Tuple2 root)
61 instance Type0_Constraint Integral (Type_Tuple2 root)
62 instance Type0_Family Type_Family_MonoElement (Type_Tuple2 root) where
63 type0_family _at (Type2 _px _a b) = Just b
64 instance Type0_Constraint MT.MonoFunctor (Type_Tuple2 root) where
65 type0_constraint _c Type2{} = Just Dict
66 instance Type1_Constraint Functor (Type_Tuple2 root) where
67 type1_constraint _c Type2{} = Just Dict
68 instance
69 Type0_Constraint Monoid root =>
70 Type1_Constraint Applicative (Type_Tuple2 root) where
71 type1_constraint _c (Type2 _ a _b)
72 | Just Dict <- type0_constraint (Proxy::Proxy Monoid) a
73 = Just Dict
74 type1_constraint _c _ = Nothing
75 instance Type1_Constraint Foldable (Type_Tuple2 root) where
76 type1_constraint _c Type2{} = Just Dict
77 instance Type1_Constraint Traversable (Type_Tuple2 root) where
78 type1_constraint _c Type2{} = Just Dict
79 instance -- Type0_Eq
80 Type0_Eq root =>
81 Type0_Eq (Type_Tuple2 root) where
82 type0_eq (Type2 _px1 a1 b1) (Type2 _px2 a2 b2)
83 | Just Refl <- a1 `type0_eq` a2
84 , Just Refl <- b1 `type0_eq` b2
85 = Just Refl
86 type0_eq _ _ = Nothing
87 instance -- Type1_Eq
88 Type0_Eq root =>
89 Type1_Eq (Type_Tuple2 root) where
90 type1_eq (Type2 _px1 a1 _b1) (Type2 _px2 a2 _b2)
91 | Just Refl <- a1 `type0_eq` a2
92 = Just Refl
93 type1_eq _ _ = Nothing
94 instance -- String_from_Type
95 String_from_Type root =>
96 String_from_Type (Type_Tuple2 root) where
97 string_from_type (Type2 _ a b) =
98 "(" ++ string_from_type a ++
99 ", " ++ string_from_type b ++ ")"
100
101 -- | Inject 'Type_Tuple2' within a root type.
102 type_tuple2
103 :: Type_Root_Lift Type_Tuple2 root
104 => root h_a -> root h_b -> root (h_a, h_b)
105 type_tuple2 = type2