]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Type/Type0.hs
init
[haskell/symantic.git] / Language / Symantic / Type / Type0.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE FlexibleInstances #-}
4 {-# LANGUAGE GADTs #-}
5 {-# LANGUAGE MultiParamTypeClasses #-}
6 {-# LANGUAGE Rank2Types #-}
7 {-# LANGUAGE ScopedTypeVariables #-}
8 {-# LANGUAGE TypeFamilies #-}
9 {-# LANGUAGE TypeOperators #-}
10 {-# LANGUAGE UndecidableInstances #-}
11 {-# OPTIONS_GHC -fno-warn-orphans #-}
12 module Language.Symantic.Type.Type0 where
13
14 import Data.Maybe (isJust)
15 import Data.Proxy
16 import Data.Type.Equality ((:~:)(Refl))
17 import GHC.Prim (Constraint)
18
19 import Language.Symantic.Lib.Data.Peano
20 import Language.Symantic.Type.Root
21 import Language.Symantic.Type.Alt
22 import Language.Symantic.Type.Error
23
24 -- * Type 'Dict'
25 -- | 'Dict' captures the dictionary of a 'Constraint':
26 -- pattern matching on the 'Dict' constructor
27 -- brings the 'Constraint' into scope.
28 data Dict :: Constraint -> * where
29 Dict :: c => Dict c
30
31 -- * Type 'No_Type'
32 -- | A discarded type.
33 data No_Type (root:: * -> *) h
34 = No_Type (root h)
35 deriving (Eq, Show)
36
37 -- * Class 'Eq_Type'
38 -- | Test two types for equality,
39 -- returning an Haskell type-level proof
40 -- of the equality when it holds.
41 class Eq_Type (ty:: * -> *) where
42 eq_type :: forall h1 h2. ty h1 -> ty h2 -> Maybe (h1 :~: h2)
43 instance -- Type_Root
44 Eq_Type (ty (Type_Root ty)) =>
45 Eq_Type (Type_Root ty) where
46 eq_type (Type_Root x) (Type_Root y) = x `eq_type` y
47 instance -- Eq Type_Root
48 Eq_Type (Type_Root ty) =>
49 Eq (Type_Root ty h) where
50 x == y = isJust $ x `eq_type` y
51 instance -- Type_Alt
52 ( Eq_Type (curr root)
53 , Eq_Type (next root)
54 ) => Eq_Type (Type_Alt curr next root) where
55 eq_type (Type_Alt_Curr x) (Type_Alt_Curr y) = x `eq_type` y
56 eq_type (Type_Alt_Next x) (Type_Alt_Next y) = x `eq_type` y
57 eq_type _ _ = Nothing
58 instance -- Eq Type_Alt
59 ( Eq_Type (curr root)
60 , Eq_Type (next root)
61 ) => Eq (Type_Alt curr next root h) where
62 x == y = isJust $ x `eq_type` y
63
64 -- * Class 'Constraint_Type'
65 -- | Test if a type satisfies a given 'Constraint',
66 -- returning an Haskell type-level proof
67 -- of that satisfaction when it holds.
68 class Constraint_Type (c:: * -> Constraint) (ty:: * -> *) where
69 constraint_type :: forall h. Proxy c -> ty h -> Maybe (Dict (c h))
70 constraint_type _c _ = Nothing
71 instance -- Type_Root
72 Constraint_Type c (ty (Type_Root ty)) =>
73 Constraint_Type c (Type_Root ty) where
74 constraint_type c (Type_Root ty) = constraint_type c ty
75 instance -- Type_Alt
76 ( Constraint_Type c (curr root)
77 , Constraint_Type c (next root)
78 ) => Constraint_Type c (Type_Alt curr next root) where
79 constraint_type c (Type_Alt_Curr ty) = constraint_type c ty
80 constraint_type c (Type_Alt_Next ty) = constraint_type c ty
81
82 -- * Class 'Type_from'
83 -- | Parse given @ast@ into a 'Root_of_Type',
84 -- or return an 'Error_of_Type'.
85 --
86 -- NOTE: making a distinction between @ty@ and 'Root_of_Type'@ ty@,
87 -- instead of having only a @root@ variable
88 -- is what enables to define many instances, one per type.
89 class Type_from ast (ty:: * -> *) where
90 type_from
91 :: Proxy ty
92 -> ast
93 -> (forall h. Root_of_Type ty h
94 -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
95 -> Either (Error_of_Type ast (Root_of_Type ty)) ret
96 instance -- Type_Root
97 ( Eq_Type (Type_Root ty)
98 , Type_from ast (ty (Type_Root ty))
99 , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
100 ) => Type_from ast (Type_Root ty) where
101 type_from _ty = type_from (Proxy::Proxy (ty (Type_Root ty)))
102 instance -- Type_Alt
103 ( Eq_Type (curr root)
104 , Type_from ast (curr root)
105 , Type_from ast (next root)
106 , Root_of_Type (curr root) ~ root
107 , Root_of_Type (next root) ~ root
108 , Unlift_Error_Type (Error_Type ast) (Error_of_Type ast root)
109 ) => Type_from ast (Type_Alt curr next root) where
110 type_from _ty ast k =
111 case type_from (Proxy::Proxy (curr root)) ast (Right . k) of
112 Right ret -> ret
113 Left err ->
114 case unlift_error_type err of
115 Just (Error_Type_Unsupported_here (_::ast)) ->
116 type_from (Proxy::Proxy (next root)) ast k
117 _ -> Left err
118
119 -- * Class 'String_from_Type'
120 -- | Return a 'String' from a type.
121 class String_from_Type ty where
122 string_from_type :: ty h -> String
123 instance -- Type_Root
124 String_from_Type (ty (Type_Root ty)) =>
125 String_from_Type (Type_Root ty) where
126 string_from_type (Type_Root ty) = string_from_type ty
127 instance -- Show Type_Root
128 String_from_Type (Type_Root ty) =>
129 Show (Type_Root ty h) where
130 show = string_from_type
131 instance -- Type_Alt
132 ( String_from_Type (curr root)
133 , String_from_Type (next root)
134 ) => String_from_Type (Type_Alt curr next root) where
135 string_from_type (Type_Alt_Curr t) = string_from_type t
136 string_from_type (Type_Alt_Next t) = string_from_type t
137
138 -- * Type 'Type_Type0'
139 -- | A type of kind @*@.
140 data Type_Type0 px (root:: * -> *) h where
141 Type_Type0 :: px -> Type_Type0 px root (Host0_of px)
142
143 type instance Root_of_Type (Type_Type0 px root) = root
144 type instance Error_of_Type ast (Type_Type0 px root) = No_Error_Type
145
146 instance -- Eq_Type
147 Eq_Type (Type_Type0 (Proxy h0) root) where
148 eq_type Type_Type0{} Type_Type0{} = Just Refl
149 instance -- Eq_Type
150 Eq_Type (Type_Type0 EPeano root) where
151 eq_type (Type_Type0 p1)
152 (Type_Type0 p2)
153 | p1 == p2
154 = Just Refl
155 eq_type _ _ = Nothing
156 instance -- Eq
157 Eq_Type (Type_Type0 px root) =>
158 Eq (Type_Type0 px root h) where
159 x == y = isJust $ x `eq_type` y
160 instance -- Show
161 String_from_Type (Type_Type0 (Proxy h0) root) =>
162 Show (Type_Type0 (Proxy h0) root h0) where
163 show = string_from_type
164 instance Eq h0 => Constraint_Type Eq (Type_Type0 (Proxy h0) root) where
165 constraint_type _c Type_Type0{} = Just Dict
166 instance Ord h0 => Constraint_Type Ord (Type_Type0 (Proxy h0) root) where
167 constraint_type _c Type_Type0{} = Just Dict
168
169 -- | Convenient alias to include a 'Type_Type0' within a type.
170 type_type0 :: forall root h0. Lift_Type_Root (Type_Type0 (Proxy h0)) root => root h0
171 type_type0 = lift_type_root (Type_Type0 (Proxy::Proxy h0))
172
173 -- ** Type family 'Host0_of'
174 type family Host0_of px :: *
175 type instance Host0_of (Proxy h0) = h0
176
177 -- ** Type 'Lift_Type'
178 -- | Apply 'Peano_of_Type' on 'Lift_TypeP'.
179 type Lift_Type ty tys
180 = Lift_TypeP (Peano_of_Type ty tys) ty tys
181 instance
182 Lift_Type ty root =>
183 Lift_Type_Root ty (Type_Root root) where
184 lift_type_root = Type_Root . lift_type
185
186 -- *** Type 'Peano_of_Type'
187 -- | Return a 'Peano' number derived from the location
188 -- of a given type within a given type stack,
189 -- which is used to avoid @OverlappingInstances@.
190 type family Peano_of_Type
191 (ty:: (* -> *) -> * -> *)
192 (tys:: (* -> *) -> * -> *) :: * where
193 Peano_of_Type ty ty = Zero
194 Peano_of_Type ty (Type_Alt ty next) = Zero
195 Peano_of_Type other (Type_Alt curr next) = Succ (Peano_of_Type other next)
196
197 -- *** Class 'Lift_TypeP'
198 -- | Lift a given type to the top of a given type stack including it,
199 -- by constructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
200 class Lift_TypeP (p:: *) ty tys where
201 lift_typeP :: forall (root:: * -> *) h. Proxy p -> ty root h -> tys root h
202 instance Lift_TypeP Zero curr curr where
203 lift_typeP _ = id
204 instance Lift_TypeP Zero curr (Type_Alt curr next) where
205 lift_typeP _ = Type_Alt_Curr
206 instance
207 Lift_TypeP p other next =>
208 Lift_TypeP (Succ p) other (Type_Alt curr next) where
209 lift_typeP _ = Type_Alt_Next . lift_typeP (Proxy::Proxy p)
210
211 -- | Convenient wrapper around 'lift_typeP',
212 -- passing it the 'Peano' number from 'Peano_of_Type'.
213 lift_type
214 :: forall ty tys (root:: * -> *) h.
215 Lift_Type ty tys =>
216 ty root h -> tys root h
217 lift_type = lift_typeP (Proxy::Proxy (Peano_of_Type ty tys))
218
219 -- ** Type 'Unlift_Type'
220 -- | Apply 'Peano_of_Type' on 'Unlift_TypeP'.
221 type Unlift_Type ty tys
222 = Unlift_TypeP (Peano_of_Type ty tys) ty tys
223
224 -- *** Class 'Unlift_TypeP'
225 -- | Try to unlift a given type out of a given type stack including it,
226 -- by deconstructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
227 class Unlift_TypeP (p:: *) ty tys where
228 type_unliftN :: forall (root:: * -> *) h. Proxy p -> tys root h -> Maybe (ty root h)
229 instance Unlift_TypeP Zero curr curr where
230 type_unliftN _ = Just
231 instance Unlift_TypeP Zero curr (Type_Alt curr next) where
232 type_unliftN _ (Type_Alt_Curr x) = Just x
233 type_unliftN _ (Type_Alt_Next _) = Nothing
234 instance
235 Unlift_TypeP p other next =>
236 Unlift_TypeP (Succ p) other (Type_Alt curr next) where
237 type_unliftN _ (Type_Alt_Next x) = type_unliftN (Proxy::Proxy p) x
238 type_unliftN _ (Type_Alt_Curr _) = Nothing
239
240 -- | Convenient wrapper around 'type_unliftN',
241 -- passing it the 'Peano' number from 'Peano_of_Type'.
242 unlift_type
243 :: forall ty tys (root:: * -> *) h.
244 Unlift_Type ty tys =>
245 tys root h -> Maybe (ty root h)
246 unlift_type = type_unliftN (Proxy::Proxy (Peano_of_Type ty tys))
247
248 -- * Type 'Exists_Type'
249 -- | Existential data type wrapping the index of a type.
250 data Exists_Type ty
251 = forall h. Exists_Type (ty h)
252 instance -- Eq
253 Eq_Type ty =>
254 Eq (Exists_Type ty) where
255 Exists_Type xh == Exists_Type yh =
256 isJust $ xh `eq_type` yh
257 instance -- Show
258 String_from_Type ty =>
259 Show (Exists_Type ty) where
260 show (Exists_Type ty) = string_from_type ty
261
262 -- * Type 'Exists_Type_and_Repr'
263 data Exists_Type_and_Repr ty repr
264 = forall h.
265 Exists_Type_and_Repr (ty h) (repr h)