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