]> Git — Sourcephile - haskell/symantic-base.git/blob - src/Symantic/Syntaxes/Data.hs
doc: rename type variable `able` to `syn`
[haskell/symantic-base.git] / src / Symantic / Syntaxes / Data.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 -- For Semantic
3 {-# LANGUAGE DataKinds #-}
4 {-# LANGUAGE GADTs #-}
5 {-# LANGUAGE PatternSynonyms #-}
6 {-# LANGUAGE RankNTypes #-}
7 {-# LANGUAGE ViewPatterns #-}
8
9 module Symantic.Syntaxes.Data where
10
11 import Data.Bool (Bool)
12 import Data.Either (Either)
13 import Data.Eq qualified as Eq
14 import Data.Function qualified as Fun
15 import Data.Maybe (Maybe)
16 import Data.Maybe qualified as Maybe
17 import Data.Semigroup (Semigroup)
18 import Type.Reflection (Typeable, eqTypeRep, typeRep, (:~~:) (..))
19
20 import Symantic.Syntaxes.Classes
21 import Symantic.Syntaxes.Derive
22
23 -- * Type 'SomeData'
24 data SomeData sem a
25 = forall syn.
26 ( Derivable (Data syn sem)
27 , Typeable syn
28 ) =>
29 SomeData (Data syn sem a)
30
31 type instance Derived (SomeData sem) = sem
32 instance Derivable (SomeData sem) where
33 derive (SomeData x) = derive x
34
35 -- ** Type 'Data'
36
37 -- TODO: neither data families nor data instances
38 -- can have phantom roles with GHC-9's RoleAnnotations,
39 -- hence 'Data.Coerce.coerce' cannot be used on them for now.
40 -- https://gitlab.haskell.org/ghc/ghc/-/issues/8177
41 -- https://gitlab.haskell.org/ghc/ghc/-/wikis/roles#proposal-roles-for-type-families
42 data family Data (syn :: Syntax) :: Semantic -> Semantic
43 type instance Derived (Data syn sem) = sem
44
45 -- | Convenient utility to pattern-match a 'SomeData'.
46 pattern Data :: Typeable syn => Data syn sem a -> SomeData sem a
47 pattern Data x <- (unSomeData -> Maybe.Just x)
48
49 -- | @(unSomeData sd :: 'Maybe' ('Data' syn sem a))@
50 -- extract the data-constructor from the given 'SomeData' @(sd)@
51 -- iif. it belongs to the @('Data' syn sem a)@ data-instance.
52 unSomeData ::
53 forall syn sem a.
54 Typeable syn =>
55 SomeData sem a ->
56 Maybe (Data syn sem a)
57 unSomeData (SomeData (constr :: Data actualSyn sem a)) =
58 case typeRep @syn `eqTypeRep` typeRep @actualSyn of
59 Maybe.Just HRefl -> Maybe.Just constr
60 Maybe.Nothing -> Maybe.Nothing
61
62 -- Abstractable
63 data instance Data Abstractable sem a where
64 Lam :: (SomeData sem a -> SomeData sem b) -> Data Abstractable sem (a -> b)
65 Lam1 :: (SomeData sem a -> SomeData sem b) -> Data Abstractable sem (a -> b)
66 Var :: sem a -> Data Abstractable sem a
67 instance Abstractable sem => Derivable (Data Abstractable sem) where
68 derive = \case
69 Lam f -> lam (\x -> derive (f (SomeData (Var x))))
70 Lam1 f -> lam1 (\x -> derive (f (SomeData (Var x))))
71 Var x -> var x
72 instance Abstractable sem => Abstractable (SomeData sem) where
73 lam f = SomeData (Lam f)
74 lam1 f = SomeData (Lam1 f)
75 var = Fun.id
76
77 -- | Beta-reduce the left-most outer-most lambda abstraction (aka. normal-order reduction),
78 -- but to avoid duplication of work, only those manually marked
79 -- as using their variable at most once.
80 --
81 -- DOC: Demonstrating Lambda Calculus Reduction, Peter Sestoft, 2001,
82 -- https://www.itu.dk/people/sestoft/papers/sestoft-lamreduce.pdf
83 normalOrderReduction ::
84 forall sem a.
85 Abstractable sem =>
86 IfThenElseable sem =>
87 SomeData sem a ->
88 SomeData sem a
89 normalOrderReduction = nor
90 where
91 nor :: SomeData sem b -> SomeData sem b
92 nor = \case
93 Data (Lam f) -> lam (nor Fun.. f)
94 Data (Lam1 f) -> lam1 (nor Fun.. f)
95 Data (x :@ y) -> case whnf x of
96 Data (Lam1 f) -> nor (f y)
97 x' -> nor x' .@ nor y
98 Data (IfThenElse test ok ko) ->
99 case nor test of
100 Data (Constant b :: Data (Constantable Bool) sem Bool) ->
101 if b then nor ok else nor ko
102 t -> ifThenElse (nor t) (nor ok) (nor ko)
103 x -> x
104
105 whnf :: SomeData sem b -> SomeData sem b
106 whnf = \case
107 Data (x :@ y) -> case whnf x of
108 Data (Lam1 f) -> whnf (f y)
109 x' -> x' .@ y
110 x -> x
111
112 -- Unabstractable
113 data instance Data Unabstractable sem a where
114 (:@) :: SomeData sem (a -> b) -> SomeData sem a -> Data Unabstractable sem b
115 instance Unabstractable sem => Derivable (Data Unabstractable sem) where
116 derive = \case
117 f :@ x -> derive f .@ derive x
118 instance Unabstractable sem => Unabstractable (SomeData sem) where
119 f .@ x = SomeData (f :@ x)
120
121 -- Functionable
122 instance
123 ( Abstractable sem
124 ) =>
125 Functionable (SomeData sem)
126 where
127 ($) = lam1 (\f -> lam1 (\x -> f .@ x))
128 (.) = lam1 (\f -> lam1 (\g -> lam1 (\x -> f .@ (g .@ x))))
129 const = lam1 (\x -> lam1 (\_y -> x))
130 flip = lam1 (\f -> lam1 (\x -> lam1 (\y -> f .@ y .@ x)))
131 id = lam1 (\x -> x)
132
133 -- Anythingable
134 data instance Data Anythingable sem a where
135 Anything :: sem a -> Data Anythingable sem a
136 instance
137 ( Anythingable sem
138 ) =>
139 Derivable (Data Anythingable sem)
140 where
141 derive = \case
142 Anything x -> anything x
143 instance Anythingable (SomeData sem)
144 instance Anythingable (Data Anythingable sem)
145
146 -- Bottomable
147 data instance Data Bottomable sem a where
148 Bottom :: Data Bottomable sem a
149 instance Bottomable sem => Derivable (Data Bottomable sem) where
150 derive Bottom{} = bottom
151
152 -- Constantable
153 data instance Data (Constantable c) sem a where
154 Constant {-Typeable c =>-} :: c -> Data (Constantable c) sem c
155 instance Constantable c sem => Derivable (Data (Constantable c) sem) where
156 derive = \case
157 Constant x -> constant x
158 instance
159 ( Constantable c sem
160 , Typeable c
161 ) =>
162 Constantable c (SomeData sem)
163 where
164 constant c = SomeData (Constant c)
165 instance{-Typeable c =>-} Constantable c (Data (Constantable c) sem) where
166 constant = Constant
167
168 -- Eitherable
169 data instance Data Eitherable sem a where
170 Either :: Data Eitherable sem ((l -> a) -> (r -> a) -> Either l r -> a)
171 Left :: Data Eitherable sem (l -> Either l r)
172 Right :: Data Eitherable sem (r -> Either l r)
173 instance Eitherable sem => Derivable (Data Eitherable sem) where
174 derive = \case
175 Either -> either
176 Left -> left
177 Right -> right
178 instance Eitherable sem => Eitherable (SomeData sem) where
179 either = SomeData Either
180 left = SomeData Left
181 right = SomeData Right
182 instance Eitherable (Data Eitherable sem) where
183 either = Either
184 left = Left
185 right = Right
186
187 -- Equalable
188 data instance Data Equalable sem a where
189 Equal :: Eq.Eq a => Data Equalable sem (a -> a -> Bool)
190 instance Equalable sem => Derivable (Data Equalable sem) where
191 derive = \case
192 Equal -> equal
193 instance
194 ( Equalable sem
195 ) =>
196 Equalable (SomeData sem)
197 where
198 equal = SomeData Equal
199 instance Equalable (Data Equalable sem) where
200 equal = Equal
201
202 -- Emptyable
203 data instance Data Emptyable sem a where
204 Empty :: Data Emptyable sem a
205 instance Emptyable sem => Derivable (Data Emptyable sem) where
206 derive = \case
207 Empty -> empty
208 instance
209 ( Emptyable sem
210 ) =>
211 Emptyable (SomeData sem)
212 where
213 empty = SomeData Empty
214 instance Emptyable (Data Emptyable sem) where
215 empty = Empty
216
217 -- Semigroupable
218 data instance Data Semigroupable sem a where
219 Concat :: Semigroup a => Data Semigroupable sem (a -> a -> a)
220 infixr 4 `Concat`
221 instance Semigroupable sem => Derivable (Data Semigroupable sem) where
222 derive = \case
223 Concat -> concat
224 instance
225 ( Semigroupable sem
226 ) =>
227 Semigroupable (SomeData sem)
228 where
229 concat = SomeData Concat
230 instance Semigroupable (Data Semigroupable sem) where
231 concat = Concat
232
233 -- IfThenElseable
234 data instance Data IfThenElseable sem a where
235 IfThenElse ::
236 SomeData sem Bool ->
237 SomeData sem a ->
238 SomeData sem a ->
239 Data IfThenElseable sem a
240 instance IfThenElseable sem => Derivable (Data IfThenElseable sem) where
241 derive = \case
242 IfThenElse test ok ko -> ifThenElse (derive test) (derive ok) (derive ko)
243 instance
244 ( IfThenElseable sem
245 ) =>
246 IfThenElseable (SomeData sem)
247 where
248 ifThenElse test ok ko = SomeData (IfThenElse test ok ko)
249 instance IfThenElseable sem => IfThenElseable (Data IfThenElseable sem) where
250 ifThenElse test ok ko = IfThenElse (SomeData test) (SomeData ok) (SomeData ko)
251
252 -- Listable
253 data instance Data Listable sem a where
254 Cons :: Data Listable sem (a -> [a] -> [a])
255 Nil :: Data Listable sem [a]
256 infixr 4 `Cons`
257 instance Listable sem => Derivable (Data Listable sem) where
258 derive = \case
259 Cons -> cons
260 Nil -> nil
261 instance
262 ( Listable sem
263 ) =>
264 Listable (SomeData sem)
265 where
266 cons = SomeData Cons
267 nil = SomeData Nil
268 instance Listable (Data Listable sem) where
269 cons = Cons
270 nil = Nil
271
272 -- Maybeable
273 data instance Data Maybeable sem a where
274 Nothing :: Data Maybeable sem (Maybe a)
275 Just :: Data Maybeable sem (a -> Maybe a)
276 instance Maybeable sem => Derivable (Data Maybeable sem) where
277 derive = \case
278 Nothing -> nothing
279 Just -> just
280 instance
281 ( Maybeable sem
282 ) =>
283 Maybeable (SomeData sem)
284 where
285 nothing = SomeData Nothing
286 just = SomeData Just
287 instance Maybeable (Data Maybeable sem) where
288 nothing = Nothing
289 just = Just