1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE DataKinds #-} -- For ReprKind
4 {-# LANGUAGE PatternSynonyms #-}
5 {-# LANGUAGE RankNTypes #-}
6 {-# LANGUAGE ViewPatterns #-}
7 module Symantic.Data where
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
20 import Symantic.Derive
23 data SomeData repr a =
25 ( Derivable (Data able repr)
27 ) => SomeData (Data able repr a)
29 type instance Derived (SomeData repr) = repr
30 instance Derivable (SomeData repr) where
31 derive (SomeData x) = derive x
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
40 (able :: ReprKind -> Constraint)
41 :: ReprKind -> ReprKind
42 type instance Derived (Data able repr) = repr
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)
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.
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
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
69 ) => Derivable (Data Abstractable repr) where
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))))
77 ) => Abstractable (SomeData repr) where
78 f .@ x = SomeData (f :@ x)
79 lam f = SomeData (Lam f)
80 lam1 f = SomeData (Lam1 f)
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)))
94 data instance Data Anythingable repr a where
95 Anything :: repr a -> Data Anythingable repr a
98 ) => Derivable (Data Anythingable repr) where
100 Anything x -> anything x
101 instance Anythingable (SomeData repr)
102 instance Anythingable (Data Anythingable repr)
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
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
115 Constant x -> constant x
117 ( Constantable c repr
119 ) => Constantable c (SomeData repr) where
120 constant c = SomeData (Constant c)
121 instance {-Typeable c =>-} Constantable c (Data (Constantable c) repr) where
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
134 ) => Eitherable (SomeData repr) where
136 right = SomeData Right
137 instance Eitherable (Data Eitherable repr) where
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
149 ) => Equalable (SomeData repr) where
150 equal = SomeData Equal
151 instance Equalable (Data Equalable repr) where
155 data instance Data Emptyable repr a where
156 Empty :: Data Emptyable repr a
157 instance Emptyable repr => Derivable (Data Emptyable repr) where
162 ) => Emptyable (SomeData repr) where
163 empty = SomeData Empty
164 instance Emptyable (Data Emptyable repr) where
168 data instance Data Semigroupable repr a where
169 Concat :: Semigroup a => Data Semigroupable repr (a -> a -> a)
171 instance Semigroupable repr => Derivable (Data Semigroupable repr) where
176 ) => Semigroupable (SomeData repr) where
177 concat = SomeData Concat
178 instance Semigroupable (Data Semigroupable repr) where
182 data instance Data IfThenElseable repr a where
184 SomeData repr Bool ->
187 Data IfThenElseable repr a
188 instance IfThenElseable repr => Derivable (Data IfThenElseable repr) where
190 IfThenElse test ok ko -> ifThenElse (derive test) (derive ok) (derive ko)
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)
199 data instance Data Listable repr a where
200 Cons :: Data Listable repr (a -> [a] -> [a])
201 Nil :: Data Listable repr [a]
203 instance Listable repr => Derivable (Data Listable repr) where
209 ) => Listable (SomeData repr) where
212 instance Listable (Data Listable repr) where
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
226 ) => Maybeable (SomeData repr) where
227 nothing = SomeData Nothing
229 instance Maybeable (Data Maybeable repr) where