]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Type/Common.hs
init
[haskell/symantic.git] / Language / Symantic / Type / Common.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE DataKinds #-}
3 {-# LANGUAGE ExistentialQuantification #-}
4 {-# LANGUAGE FlexibleContexts #-}
5 {-# LANGUAGE FlexibleInstances #-}
6 {-# LANGUAGE GADTs #-}
7 {-# LANGUAGE MultiParamTypeClasses #-}
8 {-# LANGUAGE Rank2Types #-}
9 {-# LANGUAGE ScopedTypeVariables #-}
10 {-# LANGUAGE TypeFamilies #-}
11 {-# LANGUAGE TypeOperators #-}
12 {-# LANGUAGE UndecidableInstances #-}
13 module Language.Symantic.Type.Common where
14
15 import Data.Maybe (isJust)
16 import Data.Proxy
17 import Data.Type.Equality ((:~:))
18 import Language.Symantic.Lib.Data.Peano
19 import GHC.Prim (Constraint)
20
21 -- * Class 'Eq_Type'
22
23 -- | Test two types for equality,
24 -- returning an Haskell type-level proof
25 -- of the equality when it holds.
26 class Eq_Type (ty:: * -> *) where
27 eq_type :: forall h1 h2. ty h1 -> ty h2 -> Maybe (h1 :~: h2)
28
29 -- * Class 'Constraint_Type'
30 -- | Test if a type satisfies a given 'Constraint',
31 -- returning an Haskell type-level proof
32 -- of that satisfaction when it holds.
33 class Constraint_Type (c:: * -> Constraint) (ty:: * -> *) where
34 constraint_type :: forall h. Proxy c -> ty h -> Maybe (Dict (c h))
35 constraint_type _c _ = Nothing
36
37 -- ** Type 'Dict'
38 -- | 'Dict' captures the dictionary of a 'Constraint':
39 -- pattern matching on the 'Dict' constructor
40 -- brings the 'Constraint' into scope.
41 data Dict :: Constraint -> * where
42 Dict :: c => Dict c
43
44 -- * Type 'Exists_Dict'
45 data Exists_Dict
46 = forall c. Exists_Dict (Dict c)
47
48 -- * Class 'Type_from'
49 -- | Parse given @ast@ into a 'Root_of_Type',
50 -- or return an 'Error_of_Type'.
51 class Eq_Type ty =>
52 Type_from ast (ty:: * -> *) where
53 type_from
54 :: Proxy ty
55 -> ast
56 -> (forall h. Root_of_Type ty h
57 -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
58 -> Either (Error_of_Type ast (Root_of_Type ty)) ret
59
60 -- ** Type family 'Root_of_Type'
61 -- | Return the root type of a type.
62 type family Root_of_Type (ty:: * -> *) :: * -> *
63
64 -- ** Type family 'Error_of_Type'
65 -- | Return the error type of a type.
66 type family Error_of_Type (ast:: *) (ty:: * -> *) :: *
67
68 -- * Type 'No_Type'
69 -- | A discarded type.
70 data No_Type (root:: * -> *) h
71 = No_Type (root h)
72 deriving (Eq, Show)
73
74 -- * Type 'Type_Root'
75 -- | The root type, passing itself as parameter to the given type.
76 newtype Type_Root (ty:: (* -> *) -> * -> *) h
77 = Type_Root { unType_Root :: ty (Type_Root ty) h }
78 type instance Root_of_Type (Type_Root ty) = Type_Root ty
79 -- type instance Root_of_Type (ty (Type_Root ty)) = Type_Root ty
80 type instance Error_of_Type ast (Type_Root ty)
81 = Error_Type_Alt (Error_Type ast)
82 (Error_of_Type ast (ty (Type_Root ty)))
83 instance -- Eq_Type
84 Eq_Type (ty (Type_Root ty)) =>
85 Eq_Type (Type_Root ty) where
86 eq_type (Type_Root x) (Type_Root y) = x `eq_type` y
87 instance -- Eq
88 Eq_Type (Type_Root ty) =>
89 Eq (Type_Root ty h) where
90 x == y = isJust $ x `eq_type` y
91 instance -- Constraint_Type c Type_Root
92 Constraint_Type c (ty (Type_Root ty)) =>
93 Constraint_Type c (Type_Root ty) where
94 constraint_type c (Type_Root ty) = constraint_type c ty
95 instance -- Type_from
96 ( Eq_Type (Type_Root ty)
97 , Type_from ast (ty (Type_Root ty))
98 , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
99 ) => Type_from ast (Type_Root ty) where
100 type_from _ty = type_from (Proxy::Proxy (ty (Type_Root ty)))
101 instance -- String_from_Type
102 String_from_Type (ty (Type_Root ty)) =>
103 String_from_Type (Type_Root ty) where
104 string_from_type (Type_Root ty) = string_from_type ty
105 instance -- Show
106 String_from_Type (Type_Root ty) =>
107 Show (Type_Root ty h) where
108 show = string_from_type
109
110 -- ** Class 'Type_Root_Lift'
111 -- | Lift a given type to a given root type.
112 class Type_Root_Lift ty root where
113 type_root_lift :: forall h. ty root h -> root h
114 instance
115 Type_Lift ty root =>
116 Type_Root_Lift ty (Type_Root root) where
117 type_root_lift = Type_Root . type_lift
118
119 -- * Type 'Type_Alt'
120 -- | Type making an alternative between two types.
121 data Type_Alt curr next (root:: * -> *) h
122 = Type_Alt_Curr (curr root h)
123 | Type_Alt_Next (next root h)
124 -- | Convenient alias. Requires @TypeOperators@.
125 type (:|:) = Type_Alt
126 infixr 5 :|:
127 type instance Root_of_Type (Type_Alt curr next root) = root
128 type instance Error_of_Type ast (Type_Alt curr next root)
129 = Error_of_Type_Alt ast (Error_of_Type ast (curr root))
130 (Error_of_Type ast (next root))
131 -- ** Type family 'Error_of_Type_Alt'
132 -- | Remove 'No_Type' type when building 'Error_of_Type'.
133 type family Error_of_Type_Alt ast curr next where
134 Error_of_Type_Alt ast curr No_Error_Type = curr
135 Error_of_Type_Alt ast No_Error_Type next = next
136 Error_of_Type_Alt ast curr next = Error_Type_Alt curr next
137
138 -- ** Type 'No_Error_Type'
139 -- | A discarded error.
140 data No_Error_Type
141 = No_Error_Type
142 deriving (Eq, Show)
143
144 instance -- Eq_Type
145 ( Eq_Type (curr root)
146 , Eq_Type (next root)
147 ) => Eq_Type (Type_Alt curr next root) where
148 eq_type (Type_Alt_Curr x) (Type_Alt_Curr y) = x `eq_type` y
149 eq_type (Type_Alt_Next x) (Type_Alt_Next y) = x `eq_type` y
150 eq_type _ _ = Nothing
151 instance -- Eq
152 ( Eq_Type (curr root)
153 , Eq_Type (next root)
154 ) => Eq (Type_Alt curr next root h) where
155 x == y = isJust $ x `eq_type` y
156 instance -- Constraint_Type c Type_Alt
157 ( Constraint_Type c (curr root)
158 , Constraint_Type c (next root)
159 ) => Constraint_Type c (Type_Alt curr next root) where
160 constraint_type c (Type_Alt_Curr ty) = constraint_type c ty
161 constraint_type c (Type_Alt_Next ty) = constraint_type c ty
162 instance -- Type_from
163 ( Eq_Type (curr root)
164 , Type_from ast (curr root)
165 , Type_from ast (next root)
166 , Root_of_Type (curr root) ~ root
167 , Root_of_Type (next root) ~ root
168 , Error_Type_Unlift (Error_Type ast) (Error_of_Type ast root)
169 ) => Type_from ast (Type_Alt curr next root) where
170 type_from _ty ast k =
171 case type_from (Proxy::Proxy (curr root)) ast (Right . k) of
172 Right ret -> ret
173 Left err ->
174 case error_type_unlift err of
175 Just (Error_Type_Unsupported_here (_::ast)) ->
176 type_from (Proxy::Proxy (next root)) ast k
177 _ -> Left err
178 instance -- String_from_Type
179 ( String_from_Type (curr root)
180 , String_from_Type (next root)
181 ) => String_from_Type (Type_Alt curr next root) where
182 string_from_type (Type_Alt_Curr t) = string_from_type t
183 string_from_type (Type_Alt_Next t) = string_from_type t
184
185 -- ** Type 'Type_Lift'
186 -- | Apply 'Peano_of_Type' on 'Type_LiftN'.
187 type Type_Lift ty tys
188 = Type_LiftN (Peano_of_Type ty tys) ty tys
189
190 -- *** Type 'Peano_of_Type'
191 -- | Return a 'Peano' number derived from the location
192 -- of a given type within a given type stack,
193 -- which is used to avoid @OverlappingInstances@.
194 type family Peano_of_Type
195 (ty:: (* -> *) -> * -> *)
196 (tys:: (* -> *) -> * -> *) :: * where
197 Peano_of_Type ty ty = Zero
198 Peano_of_Type ty (Type_Alt ty next) = Zero
199 Peano_of_Type other (Type_Alt curr next) = Succ (Peano_of_Type other next)
200
201 -- *** Class 'Type_LiftN'
202 -- | Lift a given type to the top of a given type stack including it,
203 -- by constructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
204 class Type_LiftN (p:: *) ty tys where
205 type_liftN :: forall (root:: * -> *) h. Proxy p -> ty root h -> tys root h
206 instance Type_LiftN Zero curr curr where
207 type_liftN _ = id
208 instance Type_LiftN Zero curr (Type_Alt curr next) where
209 type_liftN _ = Type_Alt_Curr
210 instance
211 Type_LiftN p other next =>
212 Type_LiftN (Succ p) other (Type_Alt curr next) where
213 type_liftN _ = Type_Alt_Next . type_liftN (Proxy::Proxy p)
214
215 -- | Convenient wrapper around 'type_liftN',
216 -- passing it the 'Peano' number from 'Peano_of_Type'.
217 type_lift
218 :: forall ty tys (root:: * -> *) h.
219 Type_Lift ty tys =>
220 ty root h -> tys root h
221 type_lift = type_liftN (Proxy::Proxy (Peano_of_Type ty tys))
222
223 -- ** Type 'Type_Unlift'
224 -- | Apply 'Peano_of_Type' on 'Type_UnliftN'.
225 type Type_Unlift ty tys
226 = Type_UnliftN (Peano_of_Type ty tys) ty tys
227
228 -- *** Class 'Type_UnliftN'
229 -- | Try to unlift a given type out of a given type stack including it,
230 -- by deconstructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
231 class Type_UnliftN (p:: *) ty tys where
232 type_unliftN :: forall (root:: * -> *) h. Proxy p -> tys root h -> Maybe (ty root h)
233 instance Type_UnliftN Zero curr curr where
234 type_unliftN _ = Just
235 instance Type_UnliftN Zero curr (Type_Alt curr next) where
236 type_unliftN _ (Type_Alt_Curr x) = Just x
237 type_unliftN _ (Type_Alt_Next _) = Nothing
238 instance
239 Type_UnliftN p other next =>
240 Type_UnliftN (Succ p) other (Type_Alt curr next) where
241 type_unliftN _ (Type_Alt_Next x) = type_unliftN (Proxy::Proxy p) x
242 type_unliftN _ (Type_Alt_Curr _) = Nothing
243
244 -- | Convenient wrapper around 'type_unliftN',
245 -- passing it the 'Peano' number from 'Peano_of_Type'.
246 type_unlift
247 :: forall ty tys (root:: * -> *) h.
248 Type_Unlift ty tys =>
249 tys root h -> Maybe (ty root h)
250 type_unlift = type_unliftN (Proxy::Proxy (Peano_of_Type ty tys))
251
252 -- ** Type family 'Is_Last_Type'
253 -- | Return whether a given type is the last one in a given type stack.
254 --
255 -- NOTE: each type parser uses this type family
256 -- when it encounters unsupported syntax:
257 -- to know if it is the last type parser component that will be tried
258 -- (and thus return 'Error_Type_Unsupported')
259 -- or if some other type parser component shall be tried
260 -- (and thus return 'Error_Type_Unsupported_here',
261 -- which is then handled accordingly by the 'Type_from' instance of 'Type_Alt').
262 type family Is_Last_Type (ty:: * -> *) (tys:: * -> *) :: Bool where
263 Is_Last_Type ty ty = 'True
264 Is_Last_Type ty (Type_Root tys) = Is_Last_Type ty (tys (Type_Root tys))
265 Is_Last_Type (ty root) (Type_Alt ty next root) = 'False
266 Is_Last_Type other (Type_Alt curr next root) = Is_Last_Type other (next root)
267
268 -- * Type 'Error_Type_Alt'
269 -- | Error type making an alternative between two error types.
270 data Error_Type_Alt curr next
271 = Error_Type_Alt_Curr curr
272 | Error_Type_Alt_Next next
273 deriving (Eq, Show)
274
275 -- ** Type 'Error_Type_Lift'
276 type Error_Type_Lift err errs
277 = Error_Type_LiftN (Peano_of_Error_Type err errs) err errs
278
279 -- *** Type 'Peano_of_Error_Type'
280 -- | Return a 'Peano' number derived from the location
281 -- of a given error type within a given error type stack.
282 type family Peano_of_Error_Type (err:: *) (errs:: *) :: * where
283 Peano_of_Error_Type err err = Zero
284 Peano_of_Error_Type err (Error_Type_Alt err next) = Zero
285 Peano_of_Error_Type other (Error_Type_Alt curr next) = Succ (Peano_of_Error_Type other next)
286
287 -- *** Class 'Error_Type_LiftN'
288 -- | Lift a given error type to the top of a given error type stack including it,
289 -- by constructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
290 class Error_Type_LiftN (p:: *) err errs where
291 error_type_liftN :: Proxy p -> err -> errs
292 instance Error_Type_LiftN Zero curr curr where
293 error_type_liftN _ = id
294 instance Error_Type_LiftN Zero curr (Error_Type_Alt curr next) where
295 error_type_liftN _ = Error_Type_Alt_Curr
296 instance
297 Error_Type_LiftN p other next =>
298 Error_Type_LiftN (Succ p) other (Error_Type_Alt curr next) where
299 error_type_liftN _ = Error_Type_Alt_Next . error_type_liftN (Proxy::Proxy p)
300
301 -- | Convenient wrapper around 'error_type_unliftN',
302 -- passing it the 'Peano' number from 'Peano_of_Error_Type'.
303 error_type_lift
304 :: forall err errs.
305 Error_Type_Lift err errs =>
306 err -> errs
307 error_type_lift = error_type_liftN (Proxy::Proxy (Peano_of_Error_Type err errs))
308
309 -- ** Type 'Error_Type_Unlift'
310 -- | Apply 'Peano_of_Error_Type' on 'Error_Type_UnliftN'.
311 type Error_Type_Unlift ty tys
312 = Error_Type_UnliftN (Peano_of_Error_Type ty tys) ty tys
313
314 -- | Convenient wrapper around 'error_type_unliftN',
315 -- passing it the 'Peano' number from 'Peano_of_Error_Type'.
316 error_type_unlift
317 :: forall ty tys.
318 Error_Type_Unlift ty tys =>
319 tys -> Maybe ty
320 error_type_unlift = error_type_unliftN (Proxy::Proxy (Peano_of_Error_Type ty tys))
321
322 -- *** Class 'Error_Type_UnliftN'
323 -- | Try to unlift a given type error out of a given type error stack including it,
324 -- by deconstructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
325 class Error_Type_UnliftN (p:: *) ty tys where
326 error_type_unliftN :: Proxy p -> tys -> Maybe ty
327 instance Error_Type_UnliftN Zero curr curr where
328 error_type_unliftN _ = Just
329 instance Error_Type_UnliftN Zero curr (Error_Type_Alt curr next) where
330 error_type_unliftN _ (Error_Type_Alt_Curr x) = Just x
331 error_type_unliftN _ (Error_Type_Alt_Next _) = Nothing
332 instance
333 Error_Type_UnliftN p other next =>
334 Error_Type_UnliftN (Succ p) other (Error_Type_Alt curr next) where
335 error_type_unliftN _ (Error_Type_Alt_Next x) = error_type_unliftN (Proxy::Proxy p) x
336 error_type_unliftN _ (Error_Type_Alt_Curr _) = Nothing
337
338 -- ** Type 'Error_Type_Read'
339 -- | Common type errors.
340 data Error_Type ast
341 = Error_Type_Unsupported ast
342 -- ^ Given syntax is supported by none
343 -- of the type parser components
344 -- of the type stack.
345 | Error_Type_Unsupported_here ast
346 -- ^ Given syntax not supported by the current type parser component.
347 | Error_Type_Wrong_number_of_arguments ast Int
348 deriving (Eq, Show)
349
350 -- | Convenient wrapper around 'error_type_lift',
351 -- passing the type family boilerplate.
352 error_type
353 :: Error_Type_Lift (Error_Type ast)
354 (Error_of_Type ast (Root_of_Type ty))
355 => Proxy ty
356 -> Error_Type ast
357 -> Error_of_Type ast (Root_of_Type ty)
358 error_type _ = error_type_lift
359
360 error_type_unsupported
361 :: forall ast ty.
362 ( Implicit_HBool (Is_Last_Type ty (Root_of_Type ty))
363 , Error_Type_Lift (Error_Type ast) (Error_of_Type ast (Root_of_Type ty))
364 ) => Proxy ty -> ast
365 -> Error_of_Type ast (Root_of_Type ty)
366 error_type_unsupported ty ast =
367 case hbool :: HBool (Is_Last_Type ty (Root_of_Type ty)) of
368 HTrue -> error_type ty $ Error_Type_Unsupported ast
369 HFalse -> error_type ty $ Error_Type_Unsupported_here ast
370
371 -- * Class 'String_from_Type'
372 -- | Return a 'String' from a type.
373 class String_from_Type ty where
374 string_from_type :: ty h -> String
375
376 -- * Type 'Exists_Type'
377 -- | Existential data type wrapping the index of a type.
378 data Exists_Type ty
379 = forall h. Exists_Type (ty h)
380 instance -- Eq
381 Eq_Type ty =>
382 Eq (Exists_Type ty) where
383 Exists_Type xh == Exists_Type yh =
384 isJust $ xh `eq_type` yh
385 instance -- Show
386 String_from_Type ty =>
387 Show (Exists_Type ty) where
388 show (Exists_Type ty) = string_from_type ty
389
390 -- * Type 'Exists_Type_and_Repr'
391 data Exists_Type_and_Repr ty repr
392 = forall h.
393 Exists_Type_and_Repr (ty h) (repr h)
394
395 -- * Type family 'HBool'
396 -- | Host-type equality.
397 type family HEq x y :: Bool where
398 HEq x x = 'True
399 HEq x y = 'False
400 -- ** Type 'HBool'
401 -- | Boolean singleton.
402 data HBool b where
403 HTrue :: HBool 'True
404 HFalse :: HBool 'False
405 -- ** Class 'Implicit_HBool'
406 -- | Construct a host-term boolean singleton from a host-type boolean.
407 class Implicit_HBool b where hbool :: HBool b
408 instance Implicit_HBool 'True where hbool = HTrue
409 instance Implicit_HBool 'False where hbool = HFalse