]> Git — Sourcephile - haskell/symantic-base.git/blob - src/Symantic/Data.hs
iface: add class `Inferable`
[haskell/symantic-base.git] / src / Symantic / Data.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE DataKinds #-} -- For ReprKind
3 {-# LANGUAGE GADTs #-}
4 {-# LANGUAGE PatternSynonyms #-}
5 {-# LANGUAGE RankNTypes #-}
6 {-# LANGUAGE ViewPatterns #-}
7 module Symantic.Data where
8
9 import Data.Bool (Bool)
10 import Data.Either (Either)
11 import Data.Kind (Constraint)
12 import Data.Maybe (Maybe)
13 import Data.Semigroup (Semigroup)
14 import Type.Reflection (Typeable, (:~~:)(..), eqTypeRep, typeRep)
15 import qualified Data.Eq as Eq
16 import qualified Data.Function as Fun
17 import qualified Data.Maybe as Maybe
18
19 import Symantic.Class
20 import Symantic.Derive
21
22 -- * Type 'SomeData'
23 data SomeData repr a =
24 forall able.
25 ( Derivable (Data able repr)
26 , Typeable able
27 ) => SomeData (Data able repr a)
28
29 type instance Derived (SomeData repr) = repr
30 instance Derivable (SomeData repr) where
31 derive (SomeData x) = derive x
32
33 -- ** Type 'Data'
34 -- TODO: neither data families nor data instances
35 -- can have phantom roles with GHC-9's RoleAnnotations,
36 -- hence 'Data.Coerce.coerce' cannot be used on them for now.
37 -- https://gitlab.haskell.org/ghc/ghc/-/issues/8177
38 -- https://gitlab.haskell.org/ghc/ghc/-/wikis/roles#proposal-roles-for-type-families
39 data family Data
40 (able :: ReprKind -> Constraint)
41 :: ReprKind -> ReprKind
42 type instance Derived (Data able repr) = repr
43
44 -- | Convenient utility to pattern-match a 'SomeData'.
45 pattern Data :: Typeable able => Data able repr a -> SomeData repr a
46 pattern Data x <- (unSomeData -> Maybe.Just x)
47
48 -- | @(unSomeData c :: 'Maybe' ('Data' able repr a))@
49 -- extract the data-constructor from the given 'SomeData'
50 -- iif. it belongs to the @('Data' able repr a)@ data-instance.
51 unSomeData ::
52 forall able repr a.
53 Typeable able =>
54 SomeData repr a -> Maybe (Data able repr a)
55 unSomeData (SomeData (c::Data c repr a)) =
56 case typeRep @able `eqTypeRep` typeRep @c of
57 Maybe.Just HRefl -> Maybe.Just c
58 Maybe.Nothing -> Maybe.Nothing
59
60 -- Abstractable
61 data instance Data Abstractable repr a where
62 (:@) :: SomeData repr (a->b) -> SomeData repr a -> Data Abstractable repr b
63 Lam :: (SomeData repr a -> SomeData repr b) -> Data Abstractable repr (a->b)
64 Lam1 :: (SomeData repr a -> SomeData repr b) -> Data Abstractable repr (a->b)
65 Var :: repr a -> Data Abstractable repr a
66 -- FIXME: add constructors
67 instance
68 ( Abstractable repr
69 ) => Derivable (Data Abstractable repr) where
70 derive = \case
71 f :@ x -> derive f .@ derive x
72 Lam f -> lam (\x -> derive (f (SomeData (Var x))))
73 Lam1 f -> lam1 (\x -> derive (f (SomeData (Var x))))
74 Var x -> var x
75 instance
76 ( Abstractable repr
77 ) => Abstractable (SomeData repr) where
78 f .@ x = SomeData (f :@ x)
79 lam f = SomeData (Lam f)
80 lam1 f = SomeData (Lam1 f)
81 var = Fun.id
82
83 -- Functionable
84 instance
85 ( Abstractable repr
86 ) => Functionable (SomeData repr) where
87 ($) = lam1 (\f -> lam1 (\x -> f .@ x))
88 (.) = lam1 (\f -> lam1 (\g -> lam1 (\x -> f .@ (g .@ x))))
89 const = lam1 (\x -> lam1 (\_y -> x))
90 flip = lam1 (\f -> lam1 (\x -> lam1 (\y -> f .@ y .@ x)))
91 id = lam1 (\x -> x)
92
93 -- Anythingable
94 data instance Data Anythingable repr a where
95 Anything :: repr a -> Data Anythingable repr a
96 instance
97 ( Anythingable repr
98 ) => Derivable (Data Anythingable repr) where
99 derive = \case
100 Anything x -> anything x
101 instance Anythingable (SomeData repr)
102 instance Anythingable (Data Anythingable repr)
103
104 -- Bottomable
105 data instance Data Bottomable repr a where
106 Bottom :: Data Bottomable repr a
107 instance Bottomable repr => Derivable (Data Bottomable repr) where
108 derive Bottom{} = bottom
109
110 -- Constantable
111 data instance Data (Constantable c) repr a where
112 Constant :: {-Typeable c =>-} c -> Data (Constantable c) repr c
113 instance Constantable c repr => Derivable (Data (Constantable c) repr) where
114 derive = \case
115 Constant x -> constant x
116 instance
117 ( Constantable c repr
118 , Typeable c
119 ) => Constantable c (SomeData repr) where
120 constant c = SomeData (Constant c)
121 instance {-Typeable c =>-} Constantable c (Data (Constantable c) repr) where
122 constant = Constant
123
124 -- Eitherable
125 data instance Data Eitherable repr a where
126 Left :: Data Eitherable repr (l -> Either l r)
127 Right :: Data Eitherable repr (r -> Either l r)
128 instance Eitherable repr => Derivable (Data Eitherable repr) where
129 derive = \case
130 Left -> left
131 Right -> right
132 instance
133 ( Eitherable repr
134 ) => Eitherable (SomeData repr) where
135 left = SomeData Left
136 right = SomeData Right
137 instance Eitherable (Data Eitherable repr) where
138 left = Left
139 right = Right
140
141 -- Equalable
142 data instance Data Equalable repr a where
143 Equal :: Eq.Eq a => Data Equalable repr (a -> a -> Bool)
144 instance Equalable repr => Derivable (Data Equalable repr) where
145 derive = \case
146 Equal -> equal
147 instance
148 ( Equalable repr
149 ) => Equalable (SomeData repr) where
150 equal = SomeData Equal
151 instance Equalable (Data Equalable repr) where
152 equal = Equal
153
154 -- Emptyable
155 data instance Data Emptyable repr a where
156 Empty :: Data Emptyable repr a
157 instance Emptyable repr => Derivable (Data Emptyable repr) where
158 derive = \case
159 Empty -> empty
160 instance
161 ( Emptyable repr
162 ) => Emptyable (SomeData repr) where
163 empty = SomeData Empty
164 instance Emptyable (Data Emptyable repr) where
165 empty = Empty
166
167 -- Semigroupable
168 data instance Data Semigroupable repr a where
169 Concat :: Semigroup a => Data Semigroupable repr (a -> a -> a)
170 infixr 4 `Concat`
171 instance Semigroupable repr => Derivable (Data Semigroupable repr) where
172 derive = \case
173 Concat -> concat
174 instance
175 ( Semigroupable repr
176 ) => Semigroupable (SomeData repr) where
177 concat = SomeData Concat
178 instance Semigroupable (Data Semigroupable repr) where
179 concat = Concat
180
181 -- IfThenElseable
182 data instance Data IfThenElseable repr a where
183 IfThenElse ::
184 SomeData repr Bool ->
185 SomeData repr a ->
186 SomeData repr a ->
187 Data IfThenElseable repr a
188 instance IfThenElseable repr => Derivable (Data IfThenElseable repr) where
189 derive = \case
190 IfThenElse test ok ko -> ifThenElse (derive test) (derive ok) (derive ko)
191 instance
192 ( IfThenElseable repr
193 ) => IfThenElseable (SomeData repr) where
194 ifThenElse test ok ko = SomeData (IfThenElse test ok ko)
195 instance IfThenElseable repr => IfThenElseable (Data IfThenElseable repr) where
196 ifThenElse test ok ko = IfThenElse (SomeData test) (SomeData ok) (SomeData ko)
197
198 -- Listable
199 data instance Data Listable repr a where
200 Cons :: Data Listable repr (a -> [a] -> [a])
201 Nil :: Data Listable repr [a]
202 infixr 4 `Cons`
203 instance Listable repr => Derivable (Data Listable repr) where
204 derive = \case
205 Cons -> cons
206 Nil -> nil
207 instance
208 ( Listable repr
209 ) => Listable (SomeData repr) where
210 cons = SomeData Cons
211 nil = SomeData Nil
212 instance Listable (Data Listable repr) where
213 cons = Cons
214 nil = Nil
215
216 -- Maybeable
217 data instance Data Maybeable repr a where
218 Nothing :: Data Maybeable repr (Maybe a)
219 Just :: Data Maybeable repr (a -> Maybe a)
220 instance Maybeable repr => Derivable (Data Maybeable repr) where
221 derive = \case
222 Nothing -> nothing
223 Just -> just
224 instance
225 ( Maybeable repr
226 ) => Maybeable (SomeData repr) where
227 nothing = SomeData Nothing
228 just = SomeData Just
229 instance Maybeable (Data Maybeable repr) where
230 nothing = Nothing
231 just = Just