]> Git — Sourcephile - haskell/symantic-base.git/blob - src/Symantic/Data.hs
copyright: fix REUSE
[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 StandaloneDeriving #-}
7 {-# LANGUAGE ViewPatterns #-}
8 module Symantic.Data where
9
10 import Data.Bool (Bool)
11 import Data.Either (Either)
12 import Data.Kind (Constraint)
13 import Data.Maybe (Maybe)
14 import Type.Reflection (Typeable, (:~~:)(..), eqTypeRep, typeRep)
15 import qualified Data.Eq as Eq
16 import qualified Data.Maybe as Maybe
17 import qualified Data.Function as Fun
18
19 import Symantic.Lang
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 ($) = lam1 (\f -> lam1 (\x -> f .@ x))
83 (.) = lam1 (\f -> lam1 (\g -> lam1 (\x -> f .@ (g .@ x))))
84 const = lam1 (\x -> lam1 (\_y -> x))
85 flip = lam1 (\f -> lam1 (\x -> lam1 (\y -> f .@ y .@ x)))
86 id = lam1 (\x -> x)
87
88 -- Anythingable
89 data instance Data Anythingable repr a where
90 Anything :: repr a -> Data Anythingable repr a
91 instance
92 ( Anythingable repr
93 ) =>
94 Derivable (Data Anythingable repr) where
95 derive = \case
96 Anything x -> anything x
97 instance Anythingable (SomeData repr)
98 instance Anythingable (Data Anythingable repr)
99
100 -- Bottomable
101 data instance Data Bottomable repr a where
102 Bottom :: Data Bottomable repr a
103 instance Bottomable repr => Derivable (Data Bottomable repr) where
104 derive Bottom{} = bottom
105
106 -- Constantable
107 data instance Data (Constantable c) repr a where
108 Constant :: {-Typeable c =>-} c -> Data (Constantable c) repr c
109 instance Constantable c repr => Derivable (Data (Constantable c) repr) where
110 derive = \case
111 Constant x -> constant x
112 instance
113 ( Constantable c repr
114 , Typeable c
115 ) => Constantable c (SomeData repr) where
116 constant c = SomeData (Constant c)
117 instance {-Typeable c =>-} Constantable c (Data (Constantable c) repr) where
118 constant = Constant
119
120 -- Eitherable
121 data instance Data Eitherable repr a where
122 Left :: Data Eitherable repr (l -> Either l r)
123 Right :: Data Eitherable repr (r -> Either l r)
124 instance Eitherable repr => Derivable (Data Eitherable repr) where
125 derive = \case
126 Left -> left
127 Right -> right
128 instance
129 ( Eitherable repr
130 ) => Eitherable (SomeData repr) where
131 left = SomeData Left
132 right = SomeData Right
133 instance Eitherable (Data Eitherable repr) where
134 left = Left
135 right = Right
136
137 -- Equalable
138 data instance Data Equalable repr a where
139 Equal :: Eq.Eq a => Data Equalable repr (a -> a -> Bool)
140 instance Equalable repr => Derivable (Data Equalable repr) where
141 derive = \case
142 Equal -> equal
143 instance
144 ( Equalable repr
145 ) => Equalable (SomeData repr) where
146 equal = SomeData Equal
147 instance Equalable (Data Equalable repr) where
148 equal = Equal
149
150 -- IfThenElseable
151 data instance Data IfThenElseable repr a where
152 IfThenElse ::
153 SomeData repr Bool ->
154 SomeData repr a ->
155 SomeData repr a ->
156 Data IfThenElseable repr a
157 instance IfThenElseable repr => Derivable (Data IfThenElseable repr) where
158 derive = \case
159 IfThenElse test ok ko -> ifThenElse (derive test) (derive ok) (derive ko)
160 instance
161 ( IfThenElseable repr
162 ) => IfThenElseable (SomeData repr) where
163 ifThenElse test ok ko = SomeData (IfThenElse test ok ko)
164 instance IfThenElseable repr => IfThenElseable (Data IfThenElseable repr) where
165 ifThenElse test ok ko = IfThenElse (SomeData test) (SomeData ok) (SomeData ko)
166
167 -- Listable
168 data instance Data Listable repr a where
169 Cons :: Data Listable repr (a -> [a] -> [a])
170 Nil :: Data Listable repr [a]
171 infixr 4 `Cons`
172 instance Listable repr => Derivable (Data Listable repr) where
173 derive = \case
174 Cons -> cons
175 Nil -> nil
176 instance
177 ( Listable repr
178 ) => Listable (SomeData repr) where
179 cons = SomeData Cons
180 nil = SomeData Nil
181 instance Listable (Data Listable repr) where
182 cons = Cons
183 nil = Nil
184
185 -- Maybeable
186 data instance Data Maybeable repr a where
187 Nothing :: Data Maybeable repr (Maybe a)
188 Just :: Data Maybeable repr (a -> Maybe a)
189 instance Maybeable repr => Derivable (Data Maybeable repr) where
190 derive = \case
191 Nothing -> nothing
192 Just -> just
193 instance
194 ( Maybeable repr
195 ) => Maybeable (SomeData repr) where
196 nothing = SomeData Nothing
197 just = SomeData Just
198 instance Maybeable (Data Maybeable repr) where
199 nothing = Nothing
200 just = Just