1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE DataKinds #-}
3 {-# LANGUAGE ExistentialQuantification #-}
4 {-# LANGUAGE FlexibleContexts #-}
5 {-# LANGUAGE FlexibleInstances #-}
7 {-# LANGUAGE KindSignatures #-}
8 {-# LANGUAGE PolyKinds #-}
9 {-# LANGUAGE MultiParamTypeClasses #-}
10 {-# LANGUAGE Rank2Types #-}
11 {-# LANGUAGE ScopedTypeVariables #-}
12 {-# LANGUAGE TypeFamilies #-}
13 {-# LANGUAGE TypeOperators #-}
14 {-# LANGUAGE UndecidableInstances #-}
15 module Language.LOL.Symantic.Type.Common where
17 import Data.Maybe (isJust)
19 import Data.Type.Equality ((:~:))
20 import Language.LOL.Symantic.Lib.Data.Peano
24 -- | Test two types for equality,
25 -- returning an Haskell type-level proof
26 -- of the equality when it holds.
27 class Type_Eq (ty:: k -> *) where
28 type_eq :: forall h1 h2. ty h1 -> ty h2 -> Maybe (h1 :~: h2)
30 -- * Class 'Type_from'
31 -- | Parse given @ast@ into a 'Root_of_Type',
32 -- or return an 'Error_of_Type'.
34 Type_from ast (ty:: * -> *) where
38 -> (forall h. Root_of_Type ty h
39 -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
40 -> Either (Error_of_Type ast (Root_of_Type ty)) ret
42 -- ** Type family 'Root_of_Type'
43 -- | Return the root type of a type.
44 type family Root_of_Type (ty:: * -> *) :: * -> *
46 -- ** Type family 'Error_of_Type'
47 -- | Return the error type of a type.
48 type family Error_of_Type (ast:: *) (ty:: * -> *) :: *
51 data No_Type (root:: * -> *) h
56 -- | The root type, passing itself as parameter to the given type.
57 newtype Type_Root (ty:: (* -> *) -> * -> *) h
58 = Type_Root { unType_Root :: ty (Type_Root ty) h }
59 type instance Root_of_Type (Type_Root ty) = Type_Root ty
60 -- type instance Root_of_Type (ty (Type_Root ty)) = Type_Root ty
61 type instance Error_of_Type ast (Type_Root ty)
62 = Error_Type_Alt (Error_Type ast)
63 (Error_of_Type ast (ty (Type_Root ty)))
65 Type_Eq (ty (Type_Root ty)) =>
66 Type_Eq (Type_Root ty) where
67 type_eq (Type_Root x) (Type_Root y) = x `type_eq` y
69 Type_Eq (Type_Root ty) =>
70 Eq (Type_Root ty h) where
71 x == y = isJust $ x `type_eq` y
73 ( Type_Eq (Type_Root ty)
74 , Type_from ast (ty (Type_Root ty))
75 , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
76 ) => Type_from ast (Type_Root ty) where
77 type_from _px_ty = type_from (Proxy::Proxy (ty (Type_Root ty)))
78 instance -- String_from_Type
79 String_from_Type (ty (Type_Root ty)) =>
80 String_from_Type (Type_Root ty) where
81 string_from_type (Type_Root ty) = string_from_type ty
83 String_from_Type (Type_Root ty) =>
84 Show (Type_Root ty h) where
85 show = string_from_type
87 -- ** Class 'Type_Root_Lift'
88 -- | Lift a given type to a given root type.
89 class Type_Root_Lift ty root where
90 type_root_lift :: forall h. ty root h -> root h
93 Type_Root_Lift ty (Type_Root root) where
94 type_root_lift = Type_Root . type_lift
97 -- | Type making an alternative between two types.
98 data Type_Alt curr next (root:: * -> *) h
99 = Type_Alt_Curr (curr root h)
100 | Type_Alt_Next (next root h)
101 type instance Root_of_Type (Type_Alt curr next root) = root
102 type instance Error_of_Type ast (Type_Alt curr next root)
103 = Error_of_Type_Alt ast curr next root
104 -- ** Type family 'Error_of_Type_Alt'
105 -- | Remove 'No_Type' type when building 'Error_of_Type'.
106 type family Error_of_Type_Alt ast curr next root where
107 Error_of_Type_Alt ast No_Type next root = Error_of_Type ast (next root)
108 Error_of_Type_Alt ast curr No_Type root = Error_of_Type ast (curr root)
109 Error_of_Type_Alt ast curr next root
110 = Error_Type_Alt (Error_of_Type ast (curr root))
111 (Error_of_Type ast (next root))
113 ( Type_Eq (curr root)
114 , Type_Eq (next root)
115 ) => Type_Eq (Type_Alt curr next root) where
116 type_eq (Type_Alt_Curr x) (Type_Alt_Curr y) = x `type_eq` y
117 type_eq (Type_Alt_Next x) (Type_Alt_Next y) = x `type_eq` y
118 type_eq _ _ = Nothing
120 ( Type_Eq (curr root)
121 , Type_Eq (next root)
122 ) => Eq (Type_Alt curr next root h) where
123 x == y = isJust $ x `type_eq` y
124 instance -- Type_from
125 ( Type_Eq (curr root)
126 , Type_from ast (curr root)
127 , Type_from ast (next root)
128 , Root_of_Type (curr root) ~ root
129 , Root_of_Type (next root) ~ root
130 , Error_Type_Unlift (Error_Type ast) (Error_of_Type ast root)
131 ) => Type_from ast (Type_Alt curr next root) where
132 type_from _px_ty ast k =
133 case type_from (Proxy::Proxy (curr root)) ast (Right . k) of
136 case error_type_unlift err of
137 Just (Error_Type_Unsupported_here (_::ast)) ->
138 type_from (Proxy::Proxy (next root)) ast k
140 instance -- String_from_Type
141 ( String_from_Type (curr root)
142 , String_from_Type (next root)
143 ) => String_from_Type (Type_Alt curr next root) where
144 string_from_type (Type_Alt_Curr t) = string_from_type t
145 string_from_type (Type_Alt_Next t) = string_from_type t
147 -- ** Type 'Type_Lift'
148 -- | Apply 'Peano_of_Type' on 'Type_LiftN'.
149 type Type_Lift ty tys
150 = Type_LiftN (Peano_of_Type ty tys) ty tys
152 -- *** Type 'Peano_of_Type'
153 -- | Return a 'Peano' number derived from the location
154 -- of a given type within a given type stack,
155 -- which is used to avoid @OverlappingInstances@.
156 type family Peano_of_Type
157 (ty:: (* -> *) -> * -> *)
158 (tys:: (* -> *) -> * -> *) :: * where
159 Peano_of_Type ty ty = Zero
160 Peano_of_Type ty (Type_Alt ty next) = Zero
161 Peano_of_Type other (Type_Alt curr next) = Succ (Peano_of_Type other next)
163 -- *** Class 'Type_LiftN'
164 -- | Lift a given type to the top of a given type stack including it,
165 -- by constructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
166 class Type_LiftN (p:: *) ty tys where
167 type_liftN :: forall (root:: * -> *) h. Proxy p -> ty root h -> tys root h
168 instance Type_LiftN Zero curr curr where
170 instance Type_LiftN Zero curr (Type_Alt curr next) where
171 type_liftN _ = Type_Alt_Curr
173 Type_LiftN p other next =>
174 Type_LiftN (Succ p) other (Type_Alt curr next) where
175 type_liftN _ = Type_Alt_Next . type_liftN (Proxy::Proxy p)
177 -- | Convenient wrapper around 'type_liftN',
178 -- passing it the 'Peano' number from 'Peano_of_Type'.
180 :: forall ty tys (root:: * -> *) h.
182 ty root h -> tys root h
183 type_lift = type_liftN (Proxy::Proxy (Peano_of_Type ty tys))
185 -- ** Type 'Type_Unlift'
186 -- | Apply 'Peano_of_Type' on 'Type_UnliftN'.
187 type Type_Unlift ty tys
188 = Type_UnliftN (Peano_of_Type ty tys) ty tys
190 -- *** Class 'Type_UnliftN'
191 -- | Try to unlift a given type out of a given type stack including it,
192 -- by deconstructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
193 class Type_UnliftN (p:: *) ty tys where
194 type_unliftN :: forall (root:: * -> *) h. Proxy p -> tys root h -> Maybe (ty root h)
195 instance Type_UnliftN Zero curr curr where
196 type_unliftN _ = Just
197 instance Type_UnliftN Zero curr (Type_Alt curr next) where
198 type_unliftN _ (Type_Alt_Curr x) = Just x
199 type_unliftN _ (Type_Alt_Next _) = Nothing
201 Type_UnliftN p other next =>
202 Type_UnliftN (Succ p) other (Type_Alt curr next) where
203 type_unliftN _ (Type_Alt_Next x) = type_unliftN (Proxy::Proxy p) x
204 type_unliftN _ (Type_Alt_Curr _) = Nothing
206 -- | Convenient wrapper around 'type_unliftN',
207 -- passing it the 'Peano' number from 'Peano_of_Type'.
209 :: forall ty tys (root:: * -> *) h.
210 Type_Unlift ty tys =>
211 tys root h -> Maybe (ty root h)
212 type_unlift = type_unliftN (Proxy::Proxy (Peano_of_Type ty tys))
214 -- ** Type family 'Is_Last_Type'
215 -- | Return whether a given type is the last one in a given type stack.
217 -- NOTE: each type parser uses this type family
218 -- when it encounters unsupported syntax:
219 -- to know if it is the last type parser component that will be tried
220 -- (and thus return 'Error_Type_Unsupported')
221 -- or if some other type parser component shall be tried
222 -- (and thus return 'Error_Type_Unsupported_here',
223 -- which is then handled accordingly by the 'Type_from' instance of 'Type_Alt').
224 type family Is_Last_Type (ty:: * -> *) (tys:: * -> *) :: Bool where
225 Is_Last_Type ty ty = 'True
226 Is_Last_Type ty (Type_Root tys) = Is_Last_Type ty (tys (Type_Root tys))
227 Is_Last_Type (ty root) (Type_Alt ty next root) = 'False
228 Is_Last_Type other (Type_Alt curr next root) = Is_Last_Type other (next root)
230 -- * Type 'Error_Type_Alt'
231 -- | Error type making an alternative between two error types.
232 data Error_Type_Alt curr next
233 = Error_Type_Alt_Curr curr
234 | Error_Type_Alt_Next next
237 -- ** Type 'Error_Type_Lift'
238 type Error_Type_Lift err errs
239 = Error_Type_LiftN (Peano_of_Error_Type err errs) err errs
241 -- *** Type 'Peano_of_Error_Type'
242 -- | Return a 'Peano' number derived from the location
243 -- of a given error type within a given error type stack.
244 type family Peano_of_Error_Type (err:: *) (errs:: *) :: * where
245 Peano_of_Error_Type err err = Zero
246 Peano_of_Error_Type err (Error_Type_Alt err next) = Zero
247 Peano_of_Error_Type other (Error_Type_Alt curr next) = Succ (Peano_of_Error_Type other next)
249 -- *** Class 'Error_Type_LiftN'
250 -- | Lift a given error type to the top of a given error type stack including it,
251 -- by constructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
252 class Error_Type_LiftN (p:: *) err errs where
253 error_type_liftN :: Proxy p -> err -> errs
254 instance Error_Type_LiftN Zero curr curr where
255 error_type_liftN _ = id
256 instance Error_Type_LiftN Zero curr (Error_Type_Alt curr next) where
257 error_type_liftN _ = Error_Type_Alt_Curr
259 Error_Type_LiftN p other next =>
260 Error_Type_LiftN (Succ p) other (Error_Type_Alt curr next) where
261 error_type_liftN _ = Error_Type_Alt_Next . error_type_liftN (Proxy::Proxy p)
263 -- | Convenient wrapper around 'error_type_unliftN',
264 -- passing it the 'Peano' number from 'Peano_of_Error_Type'.
267 Error_Type_Lift err errs =>
269 error_type_lift = error_type_liftN (Proxy::Proxy (Peano_of_Error_Type err errs))
271 -- ** Type 'Error_Type_Unlift'
272 -- | Apply 'Peano_of_Error_Type' on 'Error_Type_UnliftN'.
273 type Error_Type_Unlift ty tys
274 = Error_Type_UnliftN (Peano_of_Error_Type ty tys) ty tys
276 -- | Convenient wrapper around 'error_type_unliftN',
277 -- passing it the 'Peano' number from 'Peano_of_Error_Type'.
280 Error_Type_Unlift ty tys =>
282 error_type_unlift = error_type_unliftN (Proxy::Proxy (Peano_of_Error_Type ty tys))
284 -- *** Class 'Error_Type_UnliftN'
285 -- | Try to unlift a given type error out of a given type error stack including it,
286 -- by deconstructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
287 class Error_Type_UnliftN (p:: *) ty tys where
288 error_type_unliftN :: Proxy p -> tys -> Maybe ty
289 instance Error_Type_UnliftN Zero curr curr where
290 error_type_unliftN _ = Just
291 instance Error_Type_UnliftN Zero curr (Error_Type_Alt curr next) where
292 error_type_unliftN _ (Error_Type_Alt_Curr x) = Just x
293 error_type_unliftN _ (Error_Type_Alt_Next _) = Nothing
295 Error_Type_UnliftN p other next =>
296 Error_Type_UnliftN (Succ p) other (Error_Type_Alt curr next) where
297 error_type_unliftN _ (Error_Type_Alt_Next x) = error_type_unliftN (Proxy::Proxy p) x
298 error_type_unliftN _ (Error_Type_Alt_Curr _) = Nothing
300 -- ** Type 'Error_Type_Read'
301 -- | Common type errors.
303 = Error_Type_Unsupported ast
304 -- ^ Given syntax is supported by none
305 -- of the type parser components
306 -- of the type stack.
307 | Error_Type_Unsupported_here ast
308 -- ^ Given syntax not supported by the current type parser component.
309 | Error_Type_Wrong_number_of_arguments ast Int
312 -- | Convenient wrapper around 'error_type_lift',
313 -- passing the type family boilerplate.
315 :: Error_Type_Lift (Error_Type ast)
316 (Error_of_Type ast (Root_of_Type ty))
319 -> Error_of_Type ast (Root_of_Type ty)
320 error_type _ = error_type_lift
322 error_type_unsupported
324 ( Implicit_HBool (Is_Last_Type ty (Root_of_Type ty))
325 , Error_Type_Lift (Error_Type ast) (Error_of_Type ast (Root_of_Type ty))
327 -> Error_of_Type ast (Root_of_Type ty)
328 error_type_unsupported px_ty ast =
329 case hbool :: HBool (Is_Last_Type ty (Root_of_Type ty)) of
330 HTrue -> error_type px_ty $ Error_Type_Unsupported ast
331 HFalse -> error_type px_ty $ Error_Type_Unsupported_here ast
333 -- * Class 'String_from_Type'
334 -- | Return a 'String' from a type.
335 class String_from_Type ty where
336 string_from_type :: ty h -> String
338 -- * Type 'Exists_Type'
340 -- | Existential data type to wrap an indexed type.
342 = forall h. Exists_Type (ty h)
345 Eq (Exists_Type ty) where
346 Exists_Type xh == Exists_Type yh =
347 isJust $ xh `type_eq` yh
349 String_from_Type ty =>
350 Show (Exists_Type ty) where
351 show (Exists_Type ty) = string_from_type ty
353 -- * Type 'Exists_Type_and_Repr'
354 data Exists_Type_and_Repr ty repr
356 Exists_Type_and_Repr (ty h) (repr h)
358 -- * Type family 'HBool'
359 -- | Host-type equality.
360 type family HEq x y :: Bool where
364 -- | Boolean singleton.
367 HFalse :: HBool 'False
368 -- ** Class 'Implicit_HBool'
369 -- | Construct a host-term boolean singleton from a host-type boolean.
370 class Implicit_HBool b where hbool :: HBool b
371 instance Implicit_HBool 'True where hbool = HTrue
372 instance Implicit_HBool 'False where hbool = HFalse