1 {-# LANGUAGE ConstraintKinds #-}
3 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
4 {-# LANGUAGE TypeInType #-}
5 {-# LANGUAGE UndecidableInstances #-}
6 {-# LANGUAGE ViewPatterns #-}
7 {-# OPTIONS_GHC -fno-warn-orphans #-}
8 module Language.Symantic.Typing.Type where
10 import Control.Applicative (Applicative(..))
11 import qualified Data.Char as Char
12 import Data.Monoid ((<>))
14 import Data.Maybe (fromMaybe, isJust)
15 import Data.Text (Text)
16 import qualified Data.Text as Text
17 import Data.Type.Equality
18 import qualified Data.Kind as K
20 import Language.Symantic.Typing.Kind
21 import Language.Symantic.Typing.Constant
22 import Language.Symantic.Parsing
28 -- * @cs@: /type constants/, fixed at compile time.
29 -- * @h@: indexed Haskell type.
31 -- * 'TyConst': /type constant/, selected amongst @cs@.
32 -- * @(:$)@: /type application/.
34 -- See also: https://ghc.haskell.org/trac/ghc/wiki/Typeable
35 -- Which currently concludes:
36 -- "Why kind equalities, then? Given the fact that Richard's branch
37 -- doesn't solve this problem, what is it good for?
38 -- It still works wonders in the mono-kinded case,
39 -- such as for decomposing ->.
40 -- It's just that poly-kinded constructors are still a pain."
41 data Type (cs::[K.Type]) (h::k) where
42 TyConst :: TyConst cs c -> Type cs c
43 (:$) :: Type cs f -> Type cs x -> Type cs (f x)
44 -- TODO: TyVar :: SKind k -> Type cs (v::k)
47 -- | 'Type' constructor to be used
48 -- with @TypeApplications@
49 -- and @NoMonomorphismRestriction@.
50 ty :: forall c cs. Inj_TyConst cs c => Type cs c
51 ty = TyConst inj_TyConst
52 -- NOTE: The forall brings @c@ first in the type variables,
53 -- which is convenient to use @TypeApplications@.
55 instance TestEquality (Type cs) where
56 testEquality = eq_Type
57 instance Eq (Type cs h) where
59 instance Show_TyConst cs => Show (Type cs h) where
61 -- deriving instance Show_TyConst cs => Show (Type cs h)
63 kind_of :: Type cs (h::k) -> SKind k
66 TyConst c -> kind_of_TyConst c
69 _kx `SKiArrow` kf -> kf
72 :: Type cs (x::k) -> Type cs (y::k) -> Maybe (x:~:y)
73 eq_Type (TyConst x) (TyConst y)
74 | Just Refl <- testEquality x y
76 eq_Type (xf :$ xx) (yf :$ yx)
77 | Just Refl <- eq_skind (kind_of xf) (kind_of yf)
78 , Just Refl <- eq_Type xf yf
79 , Just Refl <- eq_Type xx yx
84 :: Type cs (x::kx) -> Type cs (y::ky) -> Maybe (kx:~:ky)
85 eq_Kind_Type (TyConst x) (TyConst y)
86 | Just Refl <- eq_Kind_TyConst x y
88 eq_Kind_Type (xf :$ xx) (yf :$ yx)
89 | Just Refl <- eq_Kind_Type xf yf
90 , Just Refl <- eq_Kind_Type xx yx
92 eq_Kind_Type _x _y = Nothing
94 show_Type :: Show_TyConst cs => Type cs h -> String
95 show_Type (TyConst c) = show c
96 show_Type (f@(:$){} :$ a@(:$){}) = "(" <> show_Type f <> ") (" <> show_Type a <> ")"
97 show_Type (f@(:$){} :$ a) = "(" <> show_Type f <> ") " <> show_Type a
98 show_Type (f :$ a@(:$){}) = show_Type f <> " (" <> show_Type a <> ")"
99 show_Type (f :$ a) = show_Type f <> " " <> show_Type a
100 -- show_Type (TyVar v) = "t" <> show (integral_from_peano v::Integer)
102 -- | Cons a @new_c@ to @cs@.
103 lift_Type :: Type cs c -> Type (new_c ': cs) c
104 lift_Type (TyConst c) = TyConst (TyConstS c)
105 lift_Type (f :$ a) = lift_Type f :$ lift_Type a
108 -- | Existential for 'Type'.
109 data EType cs = forall h. EType (Type cs h)
111 instance Eq (EType cs) where
113 | Just Refl <- eq_Kind_Type x y
114 = isJust $ eq_Type x y
116 instance Show_TyConst cs => Show (EType cs) where
117 show (EType t) = show t
120 -- | Existential for 'Type' of a known 'Kind'.
121 data KType cs k = forall (h::k). KType (Type cs h)
123 instance Eq (KType cs ki) where
124 KType x == KType y = isJust $ eq_Type x y
125 instance Show_TyConst cs => Show (KType cs ki) where
126 show (KType t) = show_Type t
128 -- * Type 'Token_Type'
129 type Token_Type = Type '[] ()
132 newtype TyName = TyName Text
133 deriving (Eq, Ord, Show)
135 data instance TokenT meta ts (Proxy Token_Type)
136 = Token_Type TyName [EToken meta ts]
137 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Token_Type))
138 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Token_Type))
141 ( Read_TyNameR TyName cs rs
142 , Inj_TyConst cs Token_Type
143 ) => Read_TyNameR TyName cs (Proxy Token_Type ': rs) where
144 read_TyNameR _rs (TyName "Type") k = k (ty @Token_Type)
145 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
146 instance Show_TyConst cs => Show_TyConst (Proxy Token_Type ': cs) where
147 show_TyConst TyConstZ{} = "Type"
148 show_TyConst (TyConstS c) = show_TyConst c
150 -- * Class 'Compile_Type'
151 -- | Try to build a 'Type' from name data.
152 class Compile_Type ts cs where
154 :: ( MonoLift (Error_Type meta ts) err
155 , MonoLift (Con_Kind meta ts) err )
157 -> (forall k h. Type cs (h::k) -> Either err ret)
161 :: Read_TyName TyName cs
162 => EToken meta '[Proxy Token_Type]
163 -> Either (Error_Type meta '[Proxy Token_Type]) (EType cs)
164 compile_EType tok = compile_Type tok (Right . EType)
166 -- ** Type 'Con_Kind'
167 data Con_Kind meta ts
168 = Con_Kind_Eq (At meta ts EKind) (At meta ts EKind)
169 | Con_Kind_Arrow (At meta ts EKind)
170 deriving instance (Eq_TokenR meta ts ts) => Eq (Con_Kind meta ts)
171 deriving instance (Show_TokenR meta ts ts) => Show (Con_Kind meta ts)
174 :: MonoLift (Con_Kind meta ts) err
175 => At meta ts (SKind x)
176 -> At meta ts (SKind y)
177 -> ((x :~: y) -> Either err ret) -> Either err ret
179 case unAt x `eq_skind` unAt y of
181 Nothing -> Left $ olift $
182 Con_Kind_Eq (EKind <$> x) (EKind <$> y)
185 :: MonoLift (Con_Kind meta ts) err
186 => At meta ts (SKind x)
187 -> (forall a b. (x :~: (a -> b)) -> SKind a -> SKind b -> Either err ret)
189 check_Kind_arrow x k =
191 a `SKiArrow` b -> k Refl a b
193 Con_Kind_Arrow (EKind <$> x)
195 -- ** Type 'Error_Type'
196 data Error_Type meta ts
197 = Error_Type_Token_invalid (EToken meta ts)
198 | Error_Type_Constant_unknown (At meta ts TyName)
199 | Error_Type_Con_Kind (Con_Kind meta ts)
200 deriving instance (Eq_TokenR meta ts ts) => Eq (Error_Type meta ts)
201 deriving instance (Show_TokenR meta ts ts) => Show (Error_Type meta ts)
203 -- * Class 'Read_TyName'
204 type Read_TyName raw cs = Read_TyNameR raw cs cs
207 :: forall raw cs ret.
208 Read_TyNameR raw cs cs
209 => raw -> (forall k c. Type cs (c::k) -> Maybe ret)
211 read_TyName = read_TyNameR (Proxy @cs)
213 -- ** Class 'Read_TyNameR'
214 class Read_TyNameR raw cs rs where
216 :: Proxy rs -> raw -> (forall k c. Type cs (c::k) -> Maybe ret)
219 instance Read_TyNameR raw cs '[] where
220 read_TyNameR _cs _c _k = Nothing
222 -- TODO: move each of these to a dedicated module.
224 ( Read_TyNameR TyName cs rs
225 , Inj_TyConst cs Bounded
226 ) => Read_TyNameR TyName cs (Proxy Bounded ': rs) where
227 read_TyNameR _cs (TyName "Bounded") k = k (ty @Bounded)
228 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
230 ( Read_TyNameR TyName cs rs
231 , Inj_TyConst cs Enum
232 ) => Read_TyNameR TyName cs (Proxy Enum ': rs) where
233 read_TyNameR _cs (TyName "Enum") k = k (ty @Enum)
234 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
236 ( Read_TyNameR TyName cs rs
237 , Inj_TyConst cs Fractional
238 ) => Read_TyNameR TyName cs (Proxy Fractional ': rs) where
239 read_TyNameR _cs (TyName "Fractional") k = k (ty @Fractional)
240 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
242 ( Read_TyNameR TyName cs rs
243 , Inj_TyConst cs Real
244 ) => Read_TyNameR TyName cs (Proxy Real ': rs) where
245 read_TyNameR _cs (TyName "Real") k = k (ty @Real)
246 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
248 ( Read_TyNameR TyName cs rs
250 , Inj_TyConst cs Char
251 ) => Read_TyNameR TyName cs (Proxy String ': rs) where
252 read_TyNameR _cs (TyName "String") k = k (ty @[] :$ ty @Char)
253 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
256 ( Read_TyName TyName cs
257 , Proj_Token ts Token_Type
258 ) => Compile_Type ts cs where
260 :: forall meta err ret.
261 ( MonoLift (Error_Type meta ts) err
262 , MonoLift (Con_Kind meta ts) err
264 -> (forall k h. Type cs (h::k) -> Either err ret)
266 compile_Type tok@(proj_etoken -> Just (Token_Type cst args)) kk =
267 fromMaybe (Left $ olift $ Error_Type_Constant_unknown $ At (Just tok) cst) $
268 read_TyName cst $ \typ -> Just $
271 go :: [EToken meta ts]
273 -> (forall k' h'. Type cs (h'::k') -> Either err ret)
276 go (tok_x:tok_xs) ty_f k =
277 compile_Type tok_x $ \(ty_x::Type cs (h'::k')) ->
279 (At (Just tok) $ kind_of ty_f) $ \Refl ki_f_a _ki_f_b ->
281 (At (Just tok) ki_f_a)
282 (At (Just tok_x) $ kind_of ty_x) $ \Refl ->
283 go tok_xs (ty_f :$ ty_x) k
284 compile_Type tok _k = Left $ olift $ Error_Type_Token_invalid tok
287 data Types cs (hs::[K.Type]) where
288 TypesZ :: Types cs '[]
291 -> Types cs (Proxy h ': hs)
294 eTypes :: Types cs hs -> [EType cs]
296 eTypes (TypesS t ts) = EType t : eTypes ts
298 -- | Build the left spine of a 'Type'.
301 -> (forall kc (c::kc) hs. TyConst cs c -> Types cs hs -> ret) -> ret
302 spine_of_Type (TyConst c) k = k c TypesZ
303 spine_of_Type (f :$ a) k = spine_of_Type f $ \c as -> k c (a `TypesS` as)
306 type family UnProxy (x::K.Type) :: k where
307 UnProxy (Proxy x) = x
309 -- * Class 'MonoLift'
310 class MonoLift a b where
314 (Error_Type meta ts) where
317 MonoLift (Con_Kind meta ts) (Error_Type meta ts) where
318 olift = olift . Error_Type_Con_Kind
320 -- * Class 'Gram_Type'
321 type TokType meta = EToken meta '[Proxy Token_Type]
331 ) => Gram_Type meta p where
332 typeG :: CF p (TokType meta)
333 typeG = rule "type" $ type_fun
334 type_fun :: CF p (TokType meta)
335 type_fun = rule "type_fun" $
336 infixrG type_list (metaG $ op <$ symbol "->")
337 where op meta a b = inj_EToken meta $ Token_Type (TyName "(->)") [a, b]
338 type_list :: CF p (TokType meta)
339 type_list = rule "type_list" $
341 (symbol "[") (option [] (pure <$> typeG)) (symbol "]")
342 (const <$> type_tuple2)
343 where f a meta = inj_EToken meta $ Token_Type (TyName "[]") a
344 type_tuple2 :: CF p (TokType meta)
345 type_tuple2 = rule "type_tuple2" $
346 parens (infixrG typeG (metaG $ op <$ symbol ",")) <+> type_app
347 where op meta a b = inj_EToken meta $ Token_Type (TyName "(,)") [a, b]
348 type_app :: CF p (TokType meta)
349 type_app = rule "type_app" $
352 f :: [TokType meta] -> TokType meta
353 f (EToken (TokenZ meta (Token_Type a as)):as') =
354 EToken $ TokenZ meta $ Token_Type a $ as <> as'
355 f _ = error "Oops, the impossible happened"
356 type_atom :: CF p (TokType meta)
357 type_atom = rule "type_atom" $
361 type_name :: CF p (TokType meta)
362 type_name = rule "type_name" $
364 (\c cs meta -> EToken $ TokenZ meta $ Token_Type (TyName $ Text.pack $ c:cs) [])
365 <$> unicat (Unicat Char.UppercaseLetter)
366 <*> many (choice $ unicat <$> [Unicat_Letter, Unicat_Number])
367 type_symbol :: CF p (TokType meta)
368 type_symbol = rule "type_symbol" $
370 parens $ many $ cf_of_term $ choice okG `but` choice koG
372 f s meta = inj_EToken meta $ (`Token_Type` []) $
373 TyName $ Text.concat ["(", Text.pack s, ")"]
379 koG = char <$> ['(', ')', '`']
381 deriving instance Gram_Type meta p => Gram_Type meta (CF p)
382 instance Gram_Type meta EBNF
383 instance Gram_Type meta RuleDef
385 -- | List of the rules of 'Gram_Type'.
386 gram_type :: Gram_Type meta p => [CF p (TokType meta)]