1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE DeriveFoldable #-}
3 {-# LANGUAGE DeriveFunctor #-}
4 {-# LANGUAGE DeriveTraversable #-}
5 {-# LANGUAGE EmptyDataDecls #-}
6 {-# LANGUAGE ExistentialQuantification #-}
7 {-# LANGUAGE FlexibleContexts #-}
8 {-# LANGUAGE FlexibleInstances #-}
10 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
11 {-# LANGUAGE NamedFieldPuns #-}
12 {-# LANGUAGE NoImplicitPrelude #-}
13 {-# LANGUAGE OverloadedStrings #-}
14 {-# LANGUAGE Rank2Types #-}
15 {-# LANGUAGE ScopedTypeVariables #-}
16 {-# LANGUAGE StandaloneDeriving #-}
17 {-# LANGUAGE TupleSections #-}
18 {-# LANGUAGE TypeFamilies #-}
19 {-# LANGUAGE ViewPatterns #-}
20 {-# OPTIONS_GHC -fno-warn-tabs #-}
21 module Calculus.Lambda.Omega.Explicit where
25 import qualified Data.Char as Char
26 import Data.Function (on)
27 import Data.Map.Strict (Map)
28 import qualified Data.Map.Strict as Map
29 import Data.Maybe (catMaybes)
30 import Data.Maybe (fromJust)
31 import Data.Monoid ((<>))
32 import Data.Text (Text)
33 import qualified Data.Text as Text
34 import Data.Text.Buildable (Buildable(..))
35 import qualified Data.Text.Lazy as TL
36 import qualified Data.Text.Lazy.Builder as Builder
37 import Data.Typeable as Typeable
39 import Data.Eq (Eq(..))
40 import Data.Maybe (Maybe(..), maybe)
41 import Data.Foldable (Foldable(..))
42 import Data.Either (Either(..))
43 import Data.List ((++))
44 import Data.Monoid (Monoid(..))
45 import Data.Function (($), (.), id, const, flip)
46 import Data.String (String)
47 import Data.Traversable (Traversable(..))
48 import Data.Ord (Ord(..))
49 import Control.Applicative (Applicative(..), (<$>))
50 import Text.Show (Show(..), showParen, showString)
51 import Prelude (Int, Integer, Num(..), error)
56 import Calculus.Abstraction.DeBruijn.Generalized
59 -- | 'Term' @var@ forms the main /Abstract Syntax Tree/
60 -- of the present /explicitely typed/ (aka. /à la Church/) /lambda-calculus/,
61 -- whose /term constructors/ are:
63 -- * 'TeTy_Var': for /term variable/ or /type variable/, see 'Abstraction'.
64 -- * 'TeTy_App': for /term application/ or /type application/, see 'normalize'.
65 -- * 'Term_Abst': for /term abstraction/ (aka. /λ-term/), see 'Abstraction'.
66 -- * 'Type_Abst': for /type abstraction/ (aka. /Π-type/, aka. /dependent product/), see 'sort_of_type_abst'.
67 -- * 'Type_Sort': for /sort constant/ of a /Pure Type System/ (aka. /PTS/), see 'sort_of_sort'.
68 -- * 'TeTy_Axiom': for /custom axiom/, see 'Axiomable'.
70 -- Note that 'Type' and 'Term' share this same data-type
71 -- (hence the varying prefixes of the Haskell /data constructors/),
72 -- which avoids duplication of code for their common operations.
74 -- Note that this Haskell type DOES NOT guarantee by itself
75 -- the /well-formedness/ of the 'Term' (or 'Type'),
76 -- for instance one can construct such @malformed_type@: @(* *)@:
79 -- > let star = 'Type_Sort' 'sort_star_mono'
80 -- > let malformed_type = 'TeTy_App' star star
81 -- > 'left' 'type_error_msg' '$' 'type_of' 'context' malformed_type
82 -- Left ('Type_Error_Msg_Not_a_function' … )
85 -- Though an Haskell type could be crafted to get a stronger guarantee
86 -- over the /well-formedness/, it is not done here
87 -- for the following reasons :
89 -- 1. The /well-formedness/ alone is not really useful,
90 -- it’s the /well-typedness/ which matters,
91 -- and this depends upon a specific 'Context'.
93 -- 2. Guaranteeing a good combinaison of 'TeTy_App' with respect to 'Term_Abst' (or 'Type_Abst')
94 -- while using the 'Abstraction' approach could be done:
95 -- for instance by using @GADTs@ on 'Term'
96 -- to add an Haskell /type parameter/ @ty@ (aka. /index/)
97 -- constrained to @(i -> o)@, @i@ or @o@ depending on the /term constructors/,
98 -- and then by defining Haskell /type classes/
99 -- replicating: 'Functor', 'Foldable', 'Traversable', 'Monad' and 'Monad_Module_Left',
100 -- but working on /natural transformations/ (giving /indexed functors/, /indexed monads/, …),
101 -- however this yields to a significant increase in code complexity,
102 -- which is not really worth the resulting guarantee
103 -- (to my mind, here, simplicity has priority
104 -- over comprehensive automated checking,
105 -- especially since it’s a research project
106 -- where I don't fully know all what will be needed
107 -- and thus appreciate some level of flexibility).
109 -- So, with this actual 'Term' data-type:
110 -- 'type_of' MUST be used to check the /well-formedness/ along the /well-typedness/
111 -- of a 'Term' (or equivalently of a 'Type') with respect to a 'Context'.
114 | TeTy_App (Term var) (Term var)
115 | Term_Abst (Suggest Var_Name) (Type var) (Abstraction (Suggest Var_Name) (Term) var)
116 | Type_Abst (Suggest Var_Name) (Type var) (Abstraction (Suggest Var_Name) (Type) var)
119 ( Axiomable (Axiom ax)
121 ) => TeTy_Axiom (Axiom ax)
122 -- deriving (Eq, Show, Functor, Foldable, Traversable)
123 -- | 'Eq' instance ignores /bound variables/' 'Var_Name',
124 -- effectively testing for /α-equivalence/.
125 instance (Eq var, Show var) => Eq (Term var) where
126 TeTy_Var x == TeTy_Var y = x == y
127 TeTy_App xf xa == TeTy_App yf ya = xf == yf && xa == ya
128 Term_Abst _ xty xf == Term_Abst _ yty yf = xty == yty && xf == yf -- NOTE: ignore Var_Name
129 Type_Abst _ xty xf == Type_Abst _ yty yf = xty == yty && xf == yf -- NOTE: ignore Var_Name
130 Type_Sort x == Type_Sort y = x == y
131 TeTy_Axiom x == TeTy_Axiom y = x `axiom_eq` y
133 deriving instance Show var => Show (Term var)
134 -- | A 'Functor' instance capturing the notion of /variable renaming/.
135 deriving instance Functor Term
136 deriving instance Foldable Term
137 deriving instance Traversable Term
138 deriving instance Typeable Term
139 instance Show1 Term where showsPrec1 = showsPrec
140 instance Eq1 Term where (==#) = (==)
142 instance Applicative (Term) where
145 -- | A 'Monad' instance capturing the notion of /variable substitution/ with /capture-avoiding/.
146 instance Monad (Term) where
148 Type_Sort s >>= _ = Type_Sort s
149 TeTy_Axiom a >>= _ = TeTy_Axiom a
150 TeTy_Var v >>= go = go v
151 TeTy_App f x >>= go = TeTy_App (f >>= go) (x >>= go)
152 Term_Abst v f_in f >>= go = Term_Abst v (f_in >>= go) (f >>>= go)
153 Type_Abst v f_in f >>= go = Type_Abst v (f_in >>= go) (f >>>= go)
154 instance Buildable var => Buildable (Term var) where
155 build = go False False
157 go :: forall v. (Buildable v)
161 go parenBind parenApp te =
163 Type_Sort s -> build s
164 TeTy_Axiom ax -> build ax
165 TeTy_Var v -> build v
167 (if parenApp then "(" else "")
168 <> go True False f <> " " <> go True True x
169 <> (if parenApp then ")" else "")
171 (if parenBind then "(" else "")
172 <> "λ"{- <> "\\"-} <> go_abst parenBind parenApp te
173 Type_Abst (Suggest x) f_in f_out ->
174 (if parenBind then "(" else "")
176 then go True False f_in
177 else "∀" <> "(" <> build x <> ":" <> go False False f_in <> ")" )
179 <> go False False (abstract_normalize f_out)
180 <> (if parenBind then ")" else "")
181 go_abst :: forall v. (Buildable v)
185 go_abst parenBind parenApp te =
187 Term_Abst (Suggest x) f_in f ->
188 let body = abstract_normalize f in
191 "(" <> go_var_def x <> ":" <> go False False f_in <> ")"
192 <> " " <> go_abst parenBind parenApp body
194 "(" <> go_var_def x <> ":" <> go False False f_in <> ")"
196 <> go False False body
197 <> (if parenBind then ")" else "")
198 _ -> go parenBind parenApp te
199 go_var_def x = if x == "" then "_" else build x
202 -- | Four /PTS/ /sort constants/
203 -- are formed by combining
204 -- 'Type_Level' and 'Type_Morphism':
206 -- * @*m@: the 'Sort' to form the 'Type' of a monomorphic 'Term'.
207 -- * @*p@: the 'Sort' to form the 'Type' of a polymorphic 'Term'.
208 -- * @□m@: the 'Sort' to form the 'Type' of a monomorphic 'Type'.
209 -- * @□p@: the 'Sort' to form the 'Type' of a polymorphic 'Type'.
210 type Sort = (Type_Level, Type_Morphism)
211 instance Buildable Sort where
213 (sort, morphism) -> build sort <> build morphism
215 -- | @*m@: the 'Sort' to form the 'Type' of a monomorphic 'Term'.
216 sort_star_mono :: Sort
217 sort_star_mono = (Type_Level_0, Type_Morphism_Mono)
219 -- | @*p@: the 'Sort' to form the 'Type' of a polymorphic 'Term'.
220 sort_star_poly :: Sort
221 sort_star_poly = (Type_Level_0, Type_Morphism_Poly)
223 -- *** Type 'Type_Level'
225 = Type_Level_0 -- ^ aka. /@*@ (Star) sort constant/.
226 | Type_Level_1 -- ^ aka. /@□@ (Box) sort constant/.
227 deriving (Eq, Ord, Show)
228 instance Buildable Type_Level where
233 -- *** Type 'Type_Morphism'
237 deriving (Eq, Ord, Show)
238 instance Buildable Type_Morphism where
240 Type_Morphism_Mono -> "" -- "m"
241 Type_Morphism_Poly -> "p"
243 -- | /PTS/ axioms for 'Sort':
245 -- * AXIOM: @⊦ *m : □m@
246 -- * AXIOM: @⊦ *p : □p@
247 sort_of_sort :: Sort -> Either Type_Error_Msg Sort
248 sort_of_sort (Type_Level_0, Type_Morphism_Mono)
249 = return (Type_Level_1, Type_Morphism_Mono)
251 -- The type of MONOMORPHIC types of terms,
252 -- is of type: the type of types of MONOMORPHIC types of terms
253 sort_of_sort (Type_Level_0, Type_Morphism_Poly)
254 = return (Type_Level_1, Type_Morphism_Poly)
256 -- The type of POLYMORPHIC types of terms,
257 -- is of type: the type of types of POLYMORPHIC types of terms
258 sort_of_sort s = Left $ Type_Error_Msg_No_sort_for_sort s
262 -- | A record to keep a same 'Term' (or 'Type')
263 -- in several forms (and avoid to 'normalize' it multiple times).
266 { form_given :: Term var
267 , form_normal :: Term var -- ^ 'normalize'-d version of 'form_given'.
268 } deriving (Functor, Show)
270 -- | Return a 'Form' from a given 'Term'.
271 form :: (Eq var, Ord var, Variable var, Typeable var) => Context var -> Term var -> Form var
272 form ctx te = Form te (normalize ctx te)
274 -- | Reduce given 'Term' (or 'Type') to /normal form/ (NF)
275 -- by recursively performing /β-reduction/ and /η-reduction/.
277 -- Note that any well-typed 'Term' (i.e. for which 'type_of' returns a 'Type')
278 -- is /strongly normalizing/ (i.e. 'normalize' always returns,
279 -- and its returned 'Term' is unique up to /α-equivalence/).
280 normalize :: (Eq var, Ord var, Variable var, Typeable var) => Context var -> Term var -> Term var
284 go_debug :: (Eq var, Ord var, Variable var, Typeable var)
289 go_debug args ctx te =
292 ++ "\n te = " ++ show te
293 ++ "\n args = " ++ show args
297 go :: (Eq var, Ord var, Variable var, Typeable var)
302 go args ctx (TeTy_Var ((form_normal <$>) . context_item_term <=< context_lookup ctx -> Just te))
303 -- NOTE: Replace variable mapped by the context
305 [] -> te -- NOTE: no need to normalize again
307 go args ctx (TeTy_App f x)
308 -- NOTE: Normalize and collect applied arguments,
309 -- this to normalize an argument only once for all patterns.
310 = go (go [] ctx x : args) ctx f
311 go [] ctx (Term_Abst x f_in f)
312 -- NOTE: η-reduce: Term_Abst _ (TeTy_App f (TeTy_Var (Var_Bound _)) ==> f
313 = (Term_Abst x (go [] ctx f_in) ||| id)
314 (abst_eta_reduce ctx f)
315 go (x:args) ctx (Term_Abst _ _ f)
316 -- NOTE: β-reduce: TeTy_App (Term_Abst _ _ f) x ==> f x
317 = go args ctx (const x `unabstract` f)
318 go args ctx (Type_Abst x f_in f_out)
319 -- NOTE: Recurse in Type_Abst fields
320 = term_apps (Type_Abst x (go [] ctx f_in) (go_scope ctx f_out)) args
321 go args ctx (TeTy_Axiom (flip (axiom_normalize ctx) args -> Just (r_te, r_args)))
322 -- NOTE: Normalize axiom
325 -- NOTE: Reapply remaining arguments, normalized
329 :: (Eq var, Eq bound, Ord var, Ord bound, Variable var, Variable bound, Typeable var, Typeable bound)
331 -> Abstraction bound (Term) var
332 -> Either (Abstraction bound (Term) var) -- could not η-reduce
333 (Term var) -- could η-reduce
334 abst_eta_reduce ctx =
336 let new_ctx = context_push_nothing ctx in
337 case go [] new_ctx abst_body of
338 te@(TeTy_App t (TeTy_Var (Var_Bound _{-Term_Abst's variable-}))) ->
341 Var_Free v -> Right v
342 -- NOTE: decrement the DeBruijn indexing by one
343 -- to reflect the removal of the Term_Abst.
344 Var_Bound _ -> Left $ abstract_generalize te
345 -- NOTE: cannot η-reduce because Term_Abst's variable
346 -- is also used within t.
348 te -> Left $ abstract_generalize te
353 :: (Eq var, Eq bound, Ord var, Ord bound, Variable var, Variable bound, Typeable var, Typeable bound)
355 -> Abstraction bound (Term) var
356 -> Abstraction bound (Term) var
358 abstract_generalize .
359 go [] (context_push_nothing ctx) .
362 -- | Reduce given 'Term' to /Weak Head Normal Form/ (WHNF).
366 -- * https://wiki.haskell.org/Weak_head_normal_form
367 whnf :: (Ord var, Variable var, Typeable var) => Context var -> Term var -> Term var
370 go :: (Ord var, Variable var, Typeable var) => [Term var] -> Context var -> Term var -> Term var
371 go args ctx (TeTy_Var ((form_given <$>) .
372 context_item_term <=< context_lookup ctx
374 -- NOTE: Replace any variable mapped by the context
376 go args ctx (TeTy_App f a)
377 -- NOTE: Collect applied arguments
379 go (x:args) ctx (Term_Abst _ _ f)
380 -- NOTE: β-reduce: TeTy_App (Term_Abst _ _ f) x ==> f x
381 = go args ctx (const x `unabstract` f)
382 go args ctx (TeTy_Axiom (flip (axiom_normalize ctx) args -> Just (r_te, r_args)))
383 -- NOTE: Normalize axiom
384 -- TODO: maybe introduce an 'axiom_whnf' instead of 'axiom_normalize'
387 -- NOTE: Reapply remaining arguments, normalized
390 -- | Apply multiple 'Term's to a 'Term',
391 -- useful to reconstruct a 'Term' while normalizing (see 'normalize' or 'whnf').
392 term_apps :: Term var -> [Term var] -> Term var
393 term_apps = foldl TeTy_App
395 -- | /α-equivalence relation/, synonym of @(==)@.
397 -- Return 'True' iif. both given 'Term's are the same,
398 -- up to renaming the /bound variables/ it contains (see instance 'Eq' of 'Suggest').
399 alpha_equiv :: (Eq var, Show var) => Term var -> Term var -> Bool
402 -- | /αβη-equivalence relation/.
403 equiv :: (Eq var, Ord var, Variable var, Typeable var) => Context var -> Term var -> Term var -> Bool
404 -- equiv ctx = (==) `on` (normalize ctx)
405 equiv ctx = (==) `on` normalize ctx
409 -- | 'Type' and 'Term' share the same data-type.
412 -- | Construct the 'Type' of the given 'Term',
413 -- effectively checking for the /well-formedness/
414 -- and /well-typedness/ of a 'Term' (or 'Type').
416 -- Note that a 'Type' is always to be considered
417 -- according to a given 'Context':
418 -- 'type_of' applied to the same 'Term'
419 -- but on different 'Context's
420 -- may return a different 'Type' or 'Type_Error'.
422 :: (Eq var, Ord var, Variable var, Typeable var)
425 -> Either Type_Error (Type var)
428 Type_Sort s -> (err +++ Type_Sort) $ sort_of_sort s
432 <$> context_lookup ctx v of
434 Nothing -> Left $ err $ Type_Error_Msg_Unbound_variable v
436 return $ axiom_type_of ctx ax
438 f_ty <- whnf ctx <$> type_of ctx f
441 Type_Abst _ i o -> return (i, o)
442 _ -> Left $ err $ Type_Error_Msg_Not_a_function f f_ty
443 x_ty <- type_of ctx x
444 case equiv ctx x_ty f_in of
445 True -> return $ const x `unabstract` f_out
446 False -> Left $ err $ Type_Error_Msg_Function_argument_mismatch f_in x_ty
447 Term_Abst (Suggest x) f_in f -> do
448 _ <- type_of ctx f_in
451 then context_push_nothing ctx
452 else context_push_type ctx (Suggest x) f_in
453 f_out <- type_of new_ctx (abstract_normalize f)
454 let abst_ty = Type_Abst (Suggest x) f_in (abstract_generalize f_out)
455 _ <- type_of ctx abst_ty
457 Type_Abst (Suggest x) f_in f -> do
458 f_in_ty <- type_of ctx f_in
459 f_in_so <- case whnf ctx f_in_ty of
460 Type_Sort s -> return s
461 f_in_ty_whnf -> Left $ err $ Type_Error_Msg_Invalid_input_type f_in_ty_whnf
464 then context_push_nothing ctx
465 else context_push_type ctx (Suggest x) f_in
466 f_out_ty <- type_of new_ctx (abstract_normalize f)
467 f_out_so <- case whnf new_ctx f_out_ty of
468 Type_Sort s -> return s
469 f_out_ty_whnf -> Left $ Type_Error ctx term $
470 Type_Error_Msg_Invalid_output_type f_out_ty_whnf (x, f_out_ty_whnf)
471 (err +++ Type_Sort) $
472 sort_of_type_abst f_in_so f_out_so
474 err = Type_Error ctx term
476 -- | Check that the given 'Term' has the given 'Type'.
478 :: (Eq var, Ord var, Variable var, Typeable var)
482 -> Either (Type_Error) ()
483 check ctx expect_ty te =
484 type_of ctx te >>= \actual_ty ->
485 if equiv ctx expect_ty actual_ty
487 else Left $ Type_Error
488 { type_error_ctx = ctx
489 , type_error_term = te
490 , type_error_msg = Type_Error_Msg_Type_mismatch expect_ty actual_ty (normalize ctx expect_ty) (normalize ctx actual_ty)
493 -- | Check that a 'Term' is closed, i.e. has no /unbound variables/.
494 close :: Term Var_Name -> Either Type_Error (Term ())
499 Type_Error context te $
500 Type_Error_Msg_Unbound_variable var
502 -- | Return the /unbound variables/ of given 'Term'.
503 unbound_vars :: Ord var => Term var -> Map var ()
504 unbound_vars = foldr (flip Map.insert ()) mempty
506 -- | /Dependent product/ rules: @s ↝ t : u@, i.e.
507 -- "abstracting something of type @s@ out of something of type @t@ gives something of type @u@".
509 -- Given two 'Sort': @s@ and @t@, return a 'Sort': @u@,
510 -- when ('Type_Abst' @s@ @t@) is ruled legal
511 -- and has 'Type': 'Type_Sort' ('Sort' @u@).
513 -- The usual /PTS/ rules for /λω/
514 -- (or equivalently /Type Assignment Systems/ (TAS) rules for /System Fω/)
517 -- * RULE: @⊦ * ↝ * : *@, aka. /simple types/:
518 -- "abstracting a term out of a term is valid and gives a term",
519 -- as in /PTS λ→/ or /TAS F1/.
520 -- * RULE: @⊦ □ ↝ * : *@, aka. /parametric polymorphism/:
521 -- "abstracting a type out of a term is valid and gives a term",
522 -- as in /PTS λ2/ or /TAS F2/ (aka. /System F/).
523 -- * RULE: @⊦ □ ↝ □ : □@, aka. /constructors of types/:
524 -- "abstracting a type out of a type is valid and gives a type",
525 -- as in /PTS λω/ or /TAS Fω/.
527 -- Note that the fourth usual rule is not ruled valid here:
529 -- * RULE: @⊦ * ↝ □ : □@, aka. /dependent types/:
530 -- "abstracting a term out of a type is valid and gives a type",
531 -- as in /PTS λPω/ or /TAS DFω/ (aka. /Calculus of constructions/).
533 -- However, to contain /impredicativity/ (see 'Axiom_MonoPoly')
534 -- the above /sort constants/ are split in two,
535 -- and the above rules adapted
536 -- to segregate between /monomorphic types/ (aka. /monotypes/)
537 -- and /polymorphic types/ (aka. /polytypes/):
539 -- * RULE: @⊦ *m ↝ *m : *m@, i.e. /simple types/, without /parametric polymorphism/.
540 -- * RULE: @⊦ *m ↝ *p : *p@, i.e. /simple types/, preserving /parametric polymorphism/ capture.
542 -- * RULE: @⊦ *p ↝ *m : *p@, i.e. /higher-rank polymorphism/, preserving /parametric polymorphism/ capture.
543 -- * RULE: @⊦ *p ↝ *p : *p@, i.e. /higher-rank polymorphism/, preserving /parametric polymorphism/ capture.
545 -- * RULE: @⊦ □m ↝ *m : *p@, i.e. /parametric polymorphism/, captured within @*p@ ('sort_star_poly').
546 -- * RULE: @⊦ □m ↝ *p : *p@, i.e. /parametric polymorphism/, preserving capture.
548 -- * RULE: @⊦ □m ↝ □m : □m@, i.e. /constructors of types/, without /parametric polymorphism/.
549 -- * RULE: @⊦ □m ↝ □p : □p@, i.e. /constructors of types/, preserving /parametric polymorphism/ capture.
551 -- Note that what is important here is
552 -- that there is no rule of the form: @⊦ □p ↝ _ : _@,
553 -- which forbids abstracting a /polymorphic type/ out of anything,
554 -- in particular the type @*p -> *m@ is forbidden,
555 -- though 'Axiom_MonoPoly'
556 -- is given to make it possible within it.
560 -- * /Henk: a typed intermediate language/,
561 -- Simon Peyton Jones, Erik Meijer, 20 May 1997,
562 -- https://research.microsoft.com/en-us/um/people/simonpj/papers/henk.ps.gz
566 -> Either Type_Error_Msg Sort
570 (Type_Level_0, Type_Morphism_Mono)
572 = return (Type_Level_0, m)
573 -- RULE: *m ↝ *m : *m
574 -- RULE: *m ↝ *p : *p
575 -- abstracting: a MONOMORPHIC term
576 -- out of : a MONOMORPHIC (resp. POLYMORPHIC) term
577 -- forms : a MONOMORPHIC (resp. POLYMORPHIC) term
581 (Type_Level_0, Type_Morphism_Poly)
583 = return (Type_Level_0, Type_Morphism_Poly)
584 -- RULE: *p ↝ *m : *p
585 -- RULE: *p ↝ *p : *p
586 -- abstracting: a POLYMORPHIC term
588 -- forms : a POLYMORPHIC term
592 (Type_Level_1, Type_Morphism_Mono)
594 = return (Type_Level_0, Type_Morphism_Poly)
595 -- RULE: □m ↝ *m : *p
596 -- RULE: □m ↝ *p : *p
597 -- abstracting: a MONOMORPHIC type of a term
599 -- forms : a POLYMORPHIC term
603 (Type_Level_1, Type_Morphism_Mono)
605 = return (Type_Level_1, m)
606 -- RULE: □m ↝ □m : □m
607 -- RULE: □m ↝ □p : □p
608 -- abstracting: a MONOMORPHIC type of a term
609 -- out of : a MONOMORPHIC (resp. POLYMORPHIC) type of a term
610 -- forms : a MONOMORPHIC (resp. POLYMORPHIC) type of a term
612 -- NOTE: □m ↝ □p : □p is useful for instance to build List_:
613 -- let List_ : (A:*m) -> *p = \(A:*m) -> (R:*m) -> (A -> R -> R) -> R -> R
614 -- let List : (A:*m) -> *m = \(A:*m) -> Monotype (List_ A)
620 (Type_Level_0, Type_Morphism_Mono)
622 = return (Type_Level_1, m)
623 -- RULE: *m ↝ □m : □m
624 -- RULE: *m ↝ □p : □p
625 -- abstracting: a MONOMORPHIC term
626 -- out of : a MONOMORPHIC (resp. POLYMORPHIC) type of a term
627 -- forms : a MONOMORPHIC (resp. POLYMORPHIC) type of a term
630 (Type_Level_0, Type_Morphism_Poly)
632 = return (Type_Level_1, Type_Morphism_Poly)
633 -- RULE: *p ↝ □m : □p
634 -- RULE: *p ↝ □p : □p
635 -- abstracting: a POLYMORPHIC term
636 -- out of : a type of a term
637 -- forms : a POLYMORPHIC type of a term
643 = Left $ Type_Error_Msg_Illegal_type_abstraction s t
644 -- RULE: * ↝ □ : Illegal
645 -- abstracting: a term
646 -- out of : a type of a term
649 -- No impredicativity (only allowed through 'Axiom_MonoPoly')
651 s@(Type_Level_1, Type_Morphism_Poly)
653 = Left $ Type_Error_Msg_Illegal_type_abstraction s t
654 -- RULE: □p ↝ _ : Illegal
655 -- abstracting: a POLYMORPHIC type of a term
659 -- ** Type 'Type_Error'
661 = forall var. (Ord var, Show var, Buildable var)
663 { type_error_ctx :: Context var
664 , type_error_term :: Term var
665 , type_error_msg :: Type_Error_Msg
667 deriving instance Show Type_Error
668 instance Buildable Type_Error where
669 build (Type_Error ctx te msg) =
671 <> "\n " <> build msg
672 <> "\n Term:" <> " " <> build te
678 (Map.fromList $ (, ()) <$> context_vars ctx) in
681 _ -> "\n Context:\n" <> build ctx{context_vars=vars}
684 -- ** Type 'Type_Error_Msg'
686 = Type_Error_Msg_No_sort_for_sort Sort
687 | Type_Error_Msg_Illegal_type_abstraction Sort Sort
688 | forall var. Variable var => Type_Error_Msg_Invalid_input_type (Type var)
689 | forall var. Variable var => Type_Error_Msg_Invalid_output_type (Type var) (Var_Name, Type var)
690 | forall var. Variable var => Type_Error_Msg_Not_a_function (Term var) (Type var)
691 | forall var. Variable var => Type_Error_Msg_Function_argument_mismatch (Type var) (Type var)
692 | forall var. Variable var => Type_Error_Msg_Unbound_variable var
693 | forall var. Variable var => Type_Error_Msg_Unbound_axiom var
694 | forall var. Variable var => Type_Error_Msg_Type_mismatch (Type var) (Type var) (Type var) (Type var)
695 deriving instance Show Type_Error_Msg
696 instance Buildable Type_Error_Msg where
699 Type_Error_Msg_No_sort_for_sort x ->
702 Type_Error_Msg_Illegal_type_abstraction x y ->
703 "Illegal_type_abstraction: "
704 <> build x <> " -> " <> build y
705 Type_Error_Msg_Invalid_input_type ty ->
706 "Invalid_input_type: "
708 Type_Error_Msg_Invalid_output_type f_out (x, f_in) ->
709 "Invalid_output_type: "
710 <> build f_out <> "\n"
711 <> " Input binding: "
712 <> "(" <> build x <> " : " <> build f_in <> ")"
713 Type_Error_Msg_Not_a_function f f_ty ->
718 Type_Error_Msg_Function_argument_mismatch f_in x_ty ->
719 "Function_argument_mismatch: \n"
720 <> " Function domain: " <> build f_in <> "\n"
721 <> " Argument type: " <> build x_ty
722 Type_Error_Msg_Unbound_variable var ->
725 Type_Error_Msg_Unbound_axiom var ->
728 Type_Error_Msg_Type_mismatch x y nx ny ->
730 <> " Expected type: " <> build x <> " == " <> build nx <> "\n"
731 <> " Actual type: " <> build y <> " == " <> build ny
735 -- | Map variables of type @var@
736 -- to their 'Type' and maybe also to their 'Term',
737 -- both in 'form_given' and 'form_normal'.
740 { context_vars :: [var]
741 -- ^ used to dump the 'Context'
742 , context_lookup :: var -> Maybe (Context_Item var)
743 -- ^ used to query the 'Context'
744 , context_lift :: Typeable var => Var_Name -> var
745 -- ^ used to promote a ('Term' 'Var_Name') to ('Term' @var@)
746 , context_unlift :: Typeable var => var -> Var_Name
747 -- ^ used to unpromote ('Term' @var@) to ('Term' 'Var_Name')
749 data Context_Item var
751 { context_item_term :: Maybe (Form var)
752 , context_item_type :: Form var
753 } deriving (Functor, Show)
755 instance Show var => Show (Context var) where
756 showsPrec n ctx@Context{context_vars=vars} =
758 showString "Context " .
760 (k, fromJust $ context_item_type
761 <$> context_lookup ctx k))
764 showsPrec n (catMaybes $ (\k ->
765 (k,) . form_given <$>
766 (context_item_term =<< context_lookup ctx k))
768 instance Buildable var => Buildable (Context var) where
769 build ctx@Context{context_vars=vars} =
772 <> maybe mempty (\ty -> " : " <> build (form_given ty))
773 (context_item_type <$> context_lookup ctx var)
775 <> maybe mempty (\te -> " = " <> build (form_given te))
776 (context_item_term =<< context_lookup ctx var)
781 context :: Context Var_Name
782 context = Context [] (const Nothing) id id
784 context_apply :: Context var -> Term var -> Term var
785 context_apply ctx te =
787 maybe (TeTy_Var var) id $ form_normal <$>
788 (context_item_term =<< context_lookup ctx var)
791 :: (Eq var, Ord var, Variable var, Typeable var)
795 -> Context (Var bound var)
797 ctx@(Context keys lookup var_lift var_unlift)
803 , context_lookup = \var ->
804 (Var_Free `fmap`) `fmap`
808 { context_item_term = Nothing
809 , context_item_type = form ctx ty
811 Var_Free v -> lookup v
812 , context_lift = Var_Free . var_lift
813 , context_unlift = \var ->
815 Var_Bound _ -> error "context_push_type: context_unlift"
816 Var_Free v -> var_unlift v
820 :: (Show bound, Buildable (Context var), Typeable var, Typeable bound)
822 -> Context (Var bound var)
824 (Context keys lookup var_lift var_unlift) =
826 { context_vars = Var_Free `fmap` keys
827 , context_lookup = \var ->
828 (Var_Free `fmap`) `fmap`
830 Var_Bound _ -> Nothing
831 Var_Free v -> lookup v
832 , context_lift = Var_Free . var_lift
833 , context_unlift = \var ->
835 -- DEBUG: Var_Bound (cast -> Just (Suggest b)) -> b
836 -- DEBUG: Var_Bound (cast -> Just b) -> b
837 Var_Bound b -> error $ "context_push_nothing: context_unlift: " ++ show b
838 Var_Free v -> var_unlift v
841 context_from_env :: Env -> Context Var_Name
842 context_from_env env =
844 { context_vars = Map.keys env
845 , context_lookup = \var ->
846 (\item -> Context_Item
847 { context_item_term = Just $ env_item_term item
848 , context_item_type = env_item_type item
849 }) <$> env_lookup env var
851 , context_unlift = id
854 context_relift :: forall from_var to_var.
861 context_relift from_ctx ty to_ctx =
862 ( context_lift to_ctx
863 . context_unlift from_ctx
867 context_from_list :: Eq var => [(var, Type var)] -> Context var
868 context_from_list l =
870 { context_vars = fst <$> l
871 , context_lookup_type = \var -> List.lookup var l
874 -- | Return /free term variables/ of an 'Abstraction'-ed 'Term'.
876 :: Abstraction bound (Term) var
877 -> Term (Var bound var)
878 ftv = abstract_normalize
883 = Map Var_Name Env_Item
886 { env_item_term :: Form Var_Name
887 , env_item_type :: Form Var_Name
896 { env_item_term = form ctx te
897 , env_item_type = form ctx ty
900 env_lookup :: Env -> Var_Name -> Maybe (Env_Item)
901 env_lookup env var = Map.lookup var env
903 env_insert :: Var_Name -> Term Var_Name -> Type Var_Name -> Env -> Env
904 env_insert var te ty env =
905 let ctx = context_from_env env in
906 Map.insert var (env_item ctx te ty) env
911 -- deriving instance Typeable Axiom
913 axiom_cast :: (Typeable a, Typeable b) => Axiom a -> Maybe (Axiom b)
917 -- | 'Axioms' are made of 'Axiom's injected in regular 'Env_Item's,
918 -- see 'env_item_from_axiom'.
922 :: ( Axiomable (Axiom ax)
924 => Context Var_Name -> Axiom ax -> Env_Item
925 env_item_from_axiom ctx ax =
927 { env_item_term = form ctx $ TeTy_Axiom ax
928 , env_item_type = form ctx $ axiom_type_of ctx ax
931 -- ** Class 'Axiomable'
933 -- class (Eq ax, Show ax, Buildable ax, Typeable ax) => Axiomable_Type_Of ax where
934 -- class (Eq ax, Show ax, Buildable ax, Typeable ax) => Axiomable_Normalize ax where
935 -- class (Eq ax, Show ax, Buildable ax, Typeable ax) => Axiomable_Eq ax where
937 -- | Instances of this class are 'Axiom's injectable in 'TeTy_Axiom', that is:
939 -- * they have a 'Type', given by 'axiom_type_of',
940 -- * and they can perform an optional reduction
941 -- within 'normalize' or 'whnf', given by 'axiom_normalize'.
943 ( Eq ax, Show ax, Buildable ax, Typeable ax
944 -- , Axiomable_Type_Of ax
945 -- , Axiomable_Normalize ax
947 ) => Axiomable ax where
949 :: forall var. Typeable var
950 => Context var -> ax -> Type var
951 -- ^ Return the 'Type' of the given 'Axiomable' instance.
953 :: forall var. (Typeable var, Ord var, Variable var)
954 => Context var -> ax -> [Term var] -> Maybe (Term var, [Term var])
955 -- ^ Custom-'normalize': given a typing 'Context',
956 -- an 'Axiomable' instance
957 -- and a list of arguments, return:
959 -- * 'Nothing': if the axiom performs no reduction,
960 -- * 'Just': with the reducted 'Term' and the arguments not used by the reduction.
962 -- Default: @\\_ctx _ax _args -> Nothing@
963 axiom_normalize _ctx _ax _args = Nothing
964 axiom_eq :: ax -> (forall ax'. Axiomable ax' => ax' -> Bool)
965 -- ^ Custom-bipolymorphic-@(==)@:
966 -- given an 'Axiomable' instance
967 -- return a function to test if any
968 -- other 'Axiomable' instance
969 -- is equal to the first instance given.
971 -- Default: @maybe False (x ==) (cast y)@
972 axiom_eq x y = maybe False (x ==) (cast y)
974 -- ** Class 'Axiom_Type'
976 -- | A class to embed an Haskell-type within an 'Axiom'.
977 class Axiom_Type h where
978 axiom_type :: Axiom h
979 -- ^ Construct (implicitely) an Haskell-term representing
980 -- the Haskell-type @h@.
981 axiom_Type :: Axiom h -> Type Var_Name
982 -- ^ Return a 'Type' representing the Haskell-type @h@,
983 -- given through its representation as an Haskell-term
984 -- (which is an 'Axiom' and thus has itself a 'Type',
985 -- given by its 'axiom_type_of').
988 :: (Axiom_Type h, Typeable h)
989 => h -> Axiom (Axiom_Term h)
991 Axiom_Term x $ \ctx ->
992 context_lift ctx <$> axiom_Type (axiom_type::Axiom h)
994 -- ** Type 'Axiom_Type_Assume'
995 -- | An instance to use 'Type' as an 'Axiom'.
996 data Axiom_Type_Assume
997 newtype instance Axiom (Axiom_Type_Assume)
998 = Axiom_Type_Assume (Type Var_Name)
1000 instance Buildable (Axiom Axiom_Type_Assume) where
1001 build (Axiom_Type_Assume ty) = "(_:" <> build ty <> ")"
1002 instance Axiomable (Axiom Axiom_Type_Assume) where
1003 axiom_type_of ctx (Axiom_Type_Assume ty) =
1004 context_lift ctx <$> ty
1006 -- ** Type 'Axiom_MonoPoly'
1007 -- | Non-'Sort' constants for /boxed parametric polymorphism/.
1009 -- Used to embed /polymorphic types/ into first-class /monomorphic types/
1010 -- via explicit injection ('Axiom_Term_MonoPoly_Box') and projection ('Axiom_Term_MonoPoly_UnBox') functions.
1012 -- Special treatment of 'Axiom_MonoPoly' constructors is done in 'normalize' and 'whnf'
1013 -- to remove adjacent pairs of 'Axiom_Term_MonoPoly_Box' / 'Axiom_Term_MonoPoly_UnBox'
1014 -- or 'Axiom_Term_MonoPoly_UnBox' / 'Axiom_Term_MonoPoly_Box'.
1018 -- * /Recasting MLF/, Didier Le Botlan, Didier Rémy, June 2009,
1019 -- https://hal.inria.fr/inria-00156628
1021 data instance Axiom Axiom_MonoPoly
1022 = Axiom_Type_MonoPoly
1023 | Axiom_Term_MonoPoly_Box
1024 | Axiom_Term_MonoPoly_UnBox
1025 deriving (Eq, Ord, Show)
1026 instance Buildable (Axiom Axiom_MonoPoly) where
1027 build ax = case ax of
1028 Axiom_Type_MonoPoly -> "Monotype"
1029 Axiom_Term_MonoPoly_Box -> "monotype"
1030 Axiom_Term_MonoPoly_UnBox -> "polytype"
1031 instance Axiomable (Axiom Axiom_MonoPoly) where
1032 axiom_type_of ctx ax =
1034 Axiom_Type_MonoPoly ->
1035 -- Monotype : *p -> *m
1036 Type_Abst "" (Type_Sort sort_star_poly) $
1037 (const Nothing `abstract`) $
1038 Type_Sort sort_star_mono
1039 Axiom_Term_MonoPoly_Box ->
1040 -- monotype : (Polytype : *p) -> Polytype -> Monotype Polytype
1041 (context_lift ctx <$>) $
1042 Type_Abst "Polytype" (Type_Sort sort_star_poly) $
1043 (("Polytype" =?) `abstract`) $
1044 Type_Abst "" (TeTy_Var "Polytype") $
1045 (("" =?) `abstract`) $
1047 (TeTy_Axiom $ Axiom_Type_MonoPoly)
1048 (TeTy_Var "Polytype")
1049 Axiom_Term_MonoPoly_UnBox ->
1050 -- polytype : (Polytype : *p) -> Monotype Polytype -> Polytype
1051 (context_lift ctx <$>) $
1052 Type_Abst "Polytype" (Type_Sort sort_star_poly) $
1053 (("Polytype" =?) `abstract`) $
1056 (TeTy_Axiom $ Axiom_Type_MonoPoly)
1057 (TeTy_Var "Polytype")) $
1058 (("" =?) `abstract`) $
1060 axiom_normalize _ctx
1061 Axiom_Term_MonoPoly_UnBox
1062 (_ty:TeTy_App (TeTy_App (TeTy_Axiom (axiom_cast -> Just Axiom_Term_MonoPoly_Box)) _ty') te:args)
1063 -- NOTE: Remove adjacent Axiom_Term_MonoPoly_UnBox / Axiom_Term_MonoPoly_Box
1065 axiom_normalize _ctx
1066 Axiom_Term_MonoPoly_Box
1067 (_ty:TeTy_App (TeTy_App (TeTy_Axiom (axiom_cast -> Just Axiom_Term_MonoPoly_UnBox)) _ty') te:args)
1068 -- NOTE: Remove adjacent Axiom_Term_MonoPoly_Box / Axiom_Term_MonoPoly_UnBox
1070 axiom_normalize _ctx _ax _args = Nothing
1072 -- | /PTS/ axioms for 'Axiom_MonoPoly':
1074 -- * AXIOM: @⊦ Monotype : *p -> *m@
1075 -- * AXIOM: @⊦ monotype : (Polytype : *p) -> Polytype -> Monotype Polytype@
1076 -- * AXIOM: @⊦ polytype : (Polytype : *p) -> Monotype Polytype -> Polytype@
1077 axioms_monopoly :: Axioms
1080 [ ("Monotype", item Axiom_Type_MonoPoly)
1081 , ("monotype", item Axiom_Term_MonoPoly_Box)
1082 , ("polytype", item Axiom_Term_MonoPoly_UnBox)
1085 item = env_item_from_axiom ctx
1086 ctx = context_from_env mempty
1088 -- ** Type 'Axiom_Term'
1090 -- | Embed an Haskell-term of Haskell-type @h@ within an 'Axiom'
1092 data instance Axiom (Axiom_Term h)
1095 (forall var. Typeable var => Context var -> Type var)
1098 -- Instance 'Axiom' 'Integer'
1099 data instance Axiom Integer
1100 = Axiom_Type_Integer
1101 deriving (Eq, Ord, Show)
1102 instance Buildable (Axiom Integer) where
1103 build Axiom_Type_Integer = "Int"
1104 instance Axiomable (Axiom Integer) where
1105 axiom_type_of _ctx Axiom_Type_Integer =
1106 Type_Sort (Type_Level_0, Type_Morphism_Mono)
1108 instance Axiom_Type Integer where
1109 axiom_type = Axiom_Type_Integer
1110 axiom_Type = TeTy_Axiom
1111 instance Eq (Axiom (Axiom_Term Integer)) where
1112 Axiom_Term x _ == Axiom_Term y _ = x == y
1113 instance Ord (Axiom (Axiom_Term Integer)) where
1114 Axiom_Term x _ `compare` Axiom_Term y _ = x `compare` y
1115 instance Show (Axiom (Axiom_Term Integer)) where
1116 showsPrec n (Axiom_Term te ty) =
1117 showParen (n > 10) $
1118 showString "Axiom_Term " .
1121 showsPrec n (ty context)
1122 instance Buildable (Axiom (Axiom_Term Integer)) where
1123 build (Axiom_Term i _ty) = build i
1124 instance Axiomable (Axiom (Axiom_Term Integer)) where
1125 axiom_type_of _ctx (Axiom_Term _ _ty) =
1126 TeTy_Axiom Axiom_Type_Integer
1128 -- Instance 'Axiom' '()'
1129 data instance Axiom ()
1131 deriving (Eq, Ord, Show)
1132 instance Buildable (Axiom ()) where
1133 build (Axiom_Type_Unit) = "()"
1134 instance Axiomable (Axiom ()) where
1135 axiom_type_of _ctx Axiom_Type_Unit =
1136 Type_Sort (Type_Level_0, Type_Morphism_Mono)
1138 instance Axiom_Type () where
1139 axiom_type = Axiom_Type_Unit
1140 axiom_Type = TeTy_Axiom
1141 instance Eq (Axiom (Axiom_Term ())) where
1142 Axiom_Term x _ == Axiom_Term y _ = x == y
1143 instance Ord (Axiom (Axiom_Term ())) where
1144 Axiom_Term x _ `compare` Axiom_Term y _ = x `compare` y
1145 instance Show (Axiom (Axiom_Term ())) where
1146 showsPrec n (Axiom_Term te ty) =
1147 showParen (n > 10) $
1148 showString "Axiom_Term " .
1151 showsPrec n (ty context)
1152 instance Buildable (Axiom (Axiom_Term ())) where
1153 build (Axiom_Term _te _ty) = "()"
1154 instance Axiomable (Axiom (Axiom_Term ())) where
1155 axiom_type_of _ctx (Axiom_Term _te _ty) =
1156 TeTy_Axiom Axiom_Type_Unit
1158 -- Instance 'Axiom' 'Text'
1159 data instance Axiom Text
1161 deriving (Eq, Ord, Show)
1162 instance Buildable (Axiom Text) where
1163 build (Axiom_Type_Text) = "Text"
1164 instance Axiomable (Axiom Text) where
1165 axiom_type_of _ctx Axiom_Type_Text =
1166 Type_Sort (Type_Level_0, Type_Morphism_Mono)
1168 instance Axiom_Type Text where
1169 axiom_type = Axiom_Type_Text
1170 axiom_Type = TeTy_Axiom
1171 instance Eq (Axiom (Axiom_Term Text)) where
1172 Axiom_Term x _ == Axiom_Term y _ = x == y
1173 instance Ord (Axiom (Axiom_Term Text)) where
1174 Axiom_Term x _ `compare` Axiom_Term y _ = x `compare` y
1175 instance Show (Axiom (Axiom_Term Text)) where
1176 showsPrec n (Axiom_Term te ty) =
1177 showParen (n > 10) $
1178 showString "Axiom_Term " .
1181 showsPrec n (ty context)
1182 instance Buildable (Axiom (Axiom_Term Text)) where
1183 build (Axiom_Term t _) = build $ show t
1184 instance Axiomable (Axiom (Axiom_Term Text)) where
1185 axiom_type_of _ctx (Axiom_Term _te _ty) =
1186 TeTy_Axiom Axiom_Type_Text
1188 -- Instance 'Axiom' type variable
1190 -- ** Type 'Axiom_Type_Var'
1192 -- | Singleton type, whose constructors
1193 -- are bijectively mapped to Haskell types
1194 -- of kind 'Type_Var'.
1195 data Axiom_Type_Var (v::Type_Var) where
1196 Axiom_Type_Var_Zero :: Axiom_Type_Var 'Type_Var_Zero
1197 Axiom_Type_Var_Succ :: Axiom_Type_Var v -> Axiom_Type_Var ('Type_Var_Succ v)
1198 deriving instance Eq (Axiom_Type_Var v)
1199 deriving instance Ord (Axiom_Type_Var v)
1200 deriving instance Show (Axiom_Type_Var v)
1201 deriving instance Typeable Axiom_Type_Var
1202 instance Buildable (Axiom_Type_Var v) where
1203 build v = build $ type_var_string v
1205 -- *** Type 'Type_Var'
1207 -- | Natural numbers (aka. /Peano numbers/)
1208 -- promoted by @DataKinds@ to Haskell type-level.
1211 | Type_Var_Succ Type_Var
1212 deriving (Eq, Ord, Show, Typeable)
1214 type A = Axiom_Type_Var 'Type_Var_Zero
1215 type B = Axiom_Type_Var ('Type_Var_Succ 'Type_Var_Zero)
1216 type C = Axiom_Type_Var ('Type_Var_Succ ('Type_Var_Succ 'Type_Var_Zero))
1217 -- ^ …aliases only for the first few 'Axiom_Type_Var' used: extend on need.
1219 -- | Return the Haskell term-level 'Int' encoded by the given Haskell type-level @(v :: 'Type_Var')@.
1220 type_var_int :: Axiom_Type_Var v -> Int
1223 Axiom_Type_Var_Zero -> 0
1224 Axiom_Type_Var_Succ n -> 1 + type_var_int n
1226 -- | Return a readable 'String' encoding the given Haskell type-level @(v :: 'Type_Var')@.
1228 -- First 26 variables give: @\"A"@ to @\"Z"@,
1229 -- and followings give: @(\"A" ++ show n)@, where @n@ is a positive 'Int' starting at @0@.
1230 type_var_string :: Axiom_Type_Var v -> String
1232 case type_var_int v of
1233 x | 0 <= x && x < 26 -> [Char.chr (Char.ord 'A' + x)]
1234 x -> 'A' : show (x - 26)
1236 -- *** Class 'Type_Var_Implicit'
1237 class Type_Var_Implicit (v::Type_Var) where
1238 type_var :: Axiom_Type_Var v
1239 instance Type_Var_Implicit 'Type_Var_Zero where
1240 type_var = Axiom_Type_Var_Zero
1241 instance Type_Var_Implicit v => Type_Var_Implicit ('Type_Var_Succ v) where
1242 type_var = Axiom_Type_Var_Succ type_var
1244 data instance Axiom (Axiom_Type_Var (v::Type_Var))
1245 = Axiom_Type_Var (Axiom_Type_Var v)
1246 deriving (Eq, Ord, Show)
1247 instance Buildable (Axiom (Axiom_Type_Var (v::Type_Var))) where
1248 build (Axiom_Type_Var v) = build v
1249 instance (Typeable v) => Axiomable (Axiom (Axiom_Type_Var (v::Type_Var))) where
1250 axiom_type_of _ctx (Axiom_Type_Var _v) =
1251 Type_Sort (Type_Level_0, Type_Morphism_Mono)
1252 instance Type_Var_Implicit v => Axiom_Type (Axiom_Type_Var (v::Type_Var)) where
1253 axiom_type = Axiom_Type_Var (type_var::Axiom_Type_Var v)
1254 axiom_Type (Axiom_Type_Var v) = TeTy_Var $ Text.pack $ type_var_string v
1256 instance Eq (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
1257 Axiom_Term x _ == Axiom_Term y _ = x == y
1258 instance Ord (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
1259 Axiom_Term x _ `compare` Axiom_Term y _ = x `compare` y
1260 instance Show (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
1261 showsPrec n (Axiom_Term v ty) =
1262 showParen (n > 10) $
1263 showString "Axiom_Term " .
1264 (showParen (n > 10) $
1265 showString "Axiom_Type_Var " .
1268 (showParen (n > 10) $
1270 showsPrec n (ty context))
1271 instance Buildable (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
1272 build (Axiom_Term v _ty) = build v
1273 instance Typeable v => Axiomable (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
1274 axiom_type_of ctx (Axiom_Term _ ty) = ty ctx
1276 -- Instance 'Axiom' '->'
1277 data instance Axiom (i -> o)
1278 = Axiom_Term_Abst (Axiom i) (Axiom o)
1279 deriving instance (Eq (Axiom i), Eq (Axiom o)) => Eq (Axiom (i -> o))
1280 deriving instance (Ord (Axiom i), Ord (Axiom o)) => Ord (Axiom (i -> o))
1281 deriving instance (Show (Axiom i), Show (Axiom o)) => Show (Axiom (i -> o))
1282 instance (Buildable (Axiom i), Buildable (Axiom o)) => Buildable (Axiom (i -> o)) where
1283 build (Axiom_Term_Abst i o) =
1284 "(" <> build i <> " -> " <> build o <> ")"
1290 , Buildable (Axiom i)
1293 , Buildable (Axiom o)
1294 -- , Axiomable (Axiom i)
1295 -- , Axiomable (Axiom o)
1296 ) => Axiomable (Axiom (i -> o)) where
1297 axiom_type_of _ctx (Axiom_Term_Abst _i _o) =
1298 Type_Sort (Type_Level_0, Type_Morphism_Mono)
1300 instance (Axiom_Type i, Axiom_Type o) => Axiom_Type (i -> o) where
1305 axiom_Type (Axiom_Term_Abst i o) =
1308 (const Nothing `abstract`) $
1310 instance Eq (Axiom (Axiom_Term (i -> o))) where
1311 (==) = error "Eq Axiom: (==) on functions"
1312 instance Ord (Axiom (Axiom_Term (i -> o))) where
1313 compare = error "Eq Axiom: compare on functions"
1315 {-( Buildable (Axiom (i -> o))
1316 ) =>-} Show (Axiom (Axiom_Term (i -> o))) where
1317 showsPrec n (Axiom_Term _ ty) =
1318 showParen (n > 10) $
1319 showString "Axiom_Term " .
1324 Builder.toLazyText $
1329 {-( Buildable (Axiom i)
1330 , Buildable (Axiom o)
1331 ) =>-} Buildable (Axiom (Axiom_Term (i -> o))) where
1332 build (Axiom_Term _o ty) =
1333 "(_:" <> build (ty context) <> ")"
1336 ( Typeable (Term var)
1338 , Axiomable (Axiom (Axiom_Term o))
1339 -- , Axiomable (Axiom (Term var))
1340 -- , Axiomable (Axiom o)
1341 -- , Buildable (Axiom (Term var))
1342 -- , Show (Axiom (Axiom_Term (Term var)))
1343 -- , Show (Axiom (Axiom_Term o))
1344 ) => Axiomable (Axiom (Axiom_Term (Term var -> o))) where
1345 axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
1346 axiom_normalize (ctx::Context var_)
1347 {-ax@-}(Axiom_Term (cast -> Just (o::Term var_ -> o)) o_ty)
1350 trace ("axiom_normalize (i -> o): Term"
1354 Builder.toLazyText $
1356 ++ "\n ax=" ++ show ax
1357 ++ "\n ty(ax)=" ++ show (typeOf ax)
1358 ++ "\n arg=" ++ show (context_unlift ctx <$> arg)
1359 ++ "\n args=" ++ show ((context_unlift ctx <$>) <$> args)
1360 ++ "\n o=" ++ show (Axiom_Term (o arg) o_ty)
1363 case type_of ctx arg of
1366 Type_Abst _ _o_in o_out ->
1368 let oi_ty = const i_ty `unabstract` o_out in
1369 Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
1372 axiom_normalize _ctx _ax _args = Nothing
1375 ( Typeable (Term var -> io)
1378 , Axiomable (Axiom (Axiom_Term o))
1379 -- , Axiomable (Axiom (Term var -> io))
1380 -- , Axiomable (Axiom o)
1381 -- , Show (Axiom (Axiom_Term (Term var -> io)))
1382 -- , Show (Axiom (Axiom_Term o))
1383 ) => Axiomable (Axiom (Axiom_Term ((Term var -> io) -> o))) where
1384 axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
1387 {-ax@-}(Axiom_Term (cast -> Just (o::(Term var_ -> io) -> o)) o_ty)
1388 (arg@(Term_Abst _arg_v _arg_f_in arg_f):args) =
1389 case type_of ctx arg of
1392 Type_Abst _ _o_in o_out ->
1394 trace ("axiom_normalize (i -> o): Term ->"
1398 Builder.toLazyText $
1400 ++ "\n ax=" ++ show ax
1401 ++ "\n args=" ++ show ((context_unlift ctx <$>) <$> args)
1402 ++ "\n ty(args)=" ++ show (typeOf <$> args)
1403 ++ "\n ty(ax)=" ++ show (typeOf ax)
1404 ++ "\n i~" ++ show (typeOf (undefined::Term var -> io))
1405 ++ "\n o~" ++ show (typeOf (undefined::o))
1406 ++ "\n i=" ++ show (typeOf i)
1410 case normalize ctx (const te `unabstract` arg_f) of
1411 TeTy_Axiom (axiom_cast -> Just (Axiom_Term io _io_ty)) -> io
1412 _ -> error "axiom_normalize: Axiom_Term ((Term var -> io) -> o): cannot extract io"
1415 let oi_ty = const i_ty `unabstract` o_out in
1416 Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
1421 (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
1424 Type_Abst _ _o_in o_out ->
1426 let oi_ty = const (i_ty ctx) `unabstract` o_out in
1428 trace ("axiom_normalize (i -> o): Term var -> io"
1432 Builder.toLazyText $
1433 build (context_unlift ctx <$> oi_ty))
1436 Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
1438 axiom_normalize _ctx _ax _args = Nothing
1441 ( Typeable (Axiom_Type_Var v -> io)
1443 , Axiomable (Axiom (Axiom_Type_Var v -> io))
1444 , Axiomable (Axiom o)
1445 , Axiomable (Axiom (Axiom_Term o))
1446 , Show (Axiom (Axiom_Term (Axiom_Type_Var v -> io)))
1447 , Show (Axiom (Axiom_Term o))
1448 ) => Axiomable (Axiom (Axiom_Term ((Axiom_Type_Var v -> io) -> o))) where
1449 axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
1454 , Axiomable (Axiom Integer)
1455 , Axiomable (Axiom o)
1456 , Axiomable (Axiom (Axiom_Term o))
1457 , Show (Axiom (Axiom_Term Integer))
1458 , Show (Axiom (Axiom_Term o))
1459 ) => Axiomable (Axiom (Axiom_Term (Integer -> o))) where
1460 axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
1463 (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
1466 Type_Abst _ _o_in o_out ->
1468 let oi_ty = const (i_ty ctx) `unabstract` o_out in
1470 trace ("axiom_normalize (i -> o): "
1474 Builder.toLazyText $
1475 build (context_unlift ctx <$> oi_ty))
1478 Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
1480 axiom_normalize _ctx _ax _args = Nothing
1485 , Axiomable (Axiom Text)
1486 , Axiomable (Axiom o)
1487 , Axiomable (Axiom (Axiom_Term o))
1488 , Show (Axiom (Axiom_Term Text))
1489 , Show (Axiom (Axiom_Term o))
1490 ) => Axiomable (Axiom (Axiom_Term (Text -> o))) where
1491 axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
1494 (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
1497 Type_Abst _ _o_in o_out ->
1499 let oi_ty = const (i_ty ctx) `unabstract` o_out in
1501 trace ("axiom_normalize (i -> o): "
1505 Builder.toLazyText $
1506 build (context_unlift ctx <$> oi_ty))
1509 Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
1511 axiom_normalize _ctx _ax _args = Nothing
1514 ( Typeable (Axiom_Type_Var v)
1516 , Axiomable (Axiom (Axiom_Type_Var v))
1517 , Axiomable (Axiom o)
1518 , Axiomable (Axiom (Axiom_Term o))
1519 , Show (Axiom (Axiom_Term (Axiom_Type_Var v)))
1520 , Show (Axiom (Axiom_Term o))
1521 ) => Axiomable (Axiom (Axiom_Term (Axiom_Type_Var v -> o))) where
1522 axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
1525 (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
1528 Type_Abst _ _o_in o_out ->
1530 let oi_ty = const (i_ty ctx) `unabstract` o_out in
1532 trace ("axiom_normalize (i -> o): "
1536 Builder.toLazyText $
1537 build (context_unlift ctx <$> oi_ty))
1540 Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
1542 axiom_normalize _ctx _ax _args = Nothing
1548 , Axiomable (Axiom (Axiom_Term o))
1549 , Show (Axiom (Axiom_Term (IO a)))
1550 , Show (Axiom (Axiom_Term o))
1551 -- , Axiomable (Axiom (IO a))
1552 -- , Axiomable (Axiom o)
1553 ) => Axiomable (Axiom (Axiom_Term (IO a -> o))) where
1554 axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
1557 (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
1560 Type_Abst _ _o_in o_out ->
1562 let oi_ty = const (i_ty ctx) `unabstract` o_out in
1564 trace ("axiom_normalize (Axiom_Term ((IO a) -> o)): "
1568 Builder.toLazyText $
1569 build (context_unlift ctx <$> oi_ty))
1572 Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
1574 axiom_normalize (ctx::Context var)
1576 (TeTy_Axiom (axiom_cast -> Just (Axiom_Term (i::IO (Term var)) i_ty)):args)
1579 Type_Abst _ _o_in o_out ->
1582 case normalize ctx te of
1583 TeTy_Axiom (axiom_cast -> Just (Axiom_Term io _io_ty)) -> io
1584 _ -> error "axiom_normalize: Axiom_Term ((Term var -> io) -> o): cannot extract io"
1586 let oi_ty = const (i_ty ctx) `unabstract` o_out in
1587 Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
1589 axiom_normalize _ctx _ax _args = Nothing
1591 -- ** Type 'Axiom_Type_Abst'
1593 -- | Encode a @forall a.@ within an 'Axiom'.
1594 data Axiom_Type_Abst
1595 data instance Axiom (Axiom_Type_Abst)
1597 { axiom_type_abst_Var ::
1599 -- ^ A name for the variable inhabiting the abstracting 'Type'.
1600 , axiom_type_abst_Term ::
1601 (Type Var_Name -> Term Var_Name)
1602 -- ^ The abstracted 'Term', abstracted by a 'Type'.
1603 , axiom_type_abst_Type ::
1604 (Abstraction (Suggest Var_Name) Type Var_Name)
1605 -- ^ The 'Type' of the abstracted 'Term'
1606 -- (not exactly a 'Type', but just enough to build it with 'Type_Abst').
1609 instance Eq (Axiom (Axiom_Type_Abst)) where
1610 Axiom_Type_Abst{} == Axiom_Type_Abst{} =
1611 error "Eq Axiom_Type_Abst" -- maybe False (x ==) (cast y)
1612 instance Show (Axiom (Axiom_Type_Abst)) where
1613 show (Axiom_Type_Abst{}) = "Axiom_Type_Abst"
1614 instance Buildable (Axiom (Axiom_Type_Abst)) where
1615 build ax = "(_:" <> (build $ axiom_type_of context ax) <> ")"
1616 instance Axiomable (Axiom (Axiom_Type_Abst)) where
1617 axiom_type_of ctx (Axiom_Type_Abst v _o ty) =
1619 (Type_Sort (Type_Level_0, Type_Morphism_Mono)) $
1620 (context_lift ctx <$> ty)
1622 {-ax@-}(Axiom_Type_Abst _ o ty)
1625 let a = context_unlift ctx <$> arg in
1626 let ty_a = const a `unabstract` ty in
1629 trace ("axiom_normalize: Axiom_Type_Abst:"
1633 Builder.toLazyText $
1639 Builder.toLazyText $
1640 build (axiom_type_of context ax)
1645 Builder.toLazyText $
1653 Just (context_lift ctx <$> r, args)
1654 axiom_normalize _ctx _ax _args = Nothing
1656 -- Instance 'Axiom' 'IO'
1657 data instance Axiom (IO a)
1659 deriving (Eq, Ord, Show)
1660 instance Buildable (Axiom (IO a)) where
1662 instance (Typeable a) => Axiomable (Axiom (IO a)) where
1663 axiom_type_of _ctx ax =
1667 Type_Abst "" (Type_Sort sort_star_mono) $
1668 (const Nothing `abstract`) $
1669 Type_Sort sort_star_mono
1673 ( Typeable.splitTyConApp (typeOf x)
1674 , Typeable.splitTyConApp (typeOf y)
1676 ( (xc,[(Typeable.typeRepTyCon -> xc')])
1677 , (yc,[(Typeable.typeRepTyCon -> yc')])
1678 ) | xc == yc && xc' == yc' -> True
1680 error $ "Eq: Axiomable (Axiom (IO a)): "
1681 ++ "\n x : " ++ show (Typeable.splitTyConApp (typeOf x))
1682 ++ "\n y : " ++ show (Typeable.splitTyConApp (typeOf y))
1688 ) => Axiom_Type (IO a) where
1689 axiom_type = Axiom_Type_IO
1690 axiom_Type (Axiom_Type_IO) =
1692 (TeTy_Axiom (Axiom_Type_IO::Axiom (IO a)))
1693 (axiom_Type (axiom_type::Axiom a))
1695 instance Eq (Axiom (Axiom_Term (IO a))) where
1696 (==) = error "Eq Axiom: (==) on IO"
1697 instance Ord (Axiom (Axiom_Term (IO a))) where
1698 compare = error "Eq Axiom: compare on IO"
1700 {-( Buildable (Axiom a)
1701 ) =>-} Show (Axiom (Axiom_Term (IO a))) where
1702 showsPrec n (Axiom_Term _te ty) =
1703 showParen (n > 10) $
1704 showString "Axiom_Term " .
1709 Builder.toLazyText $
1710 build $ (ty context)
1714 {-( Buildable (Axiom a)
1715 ) =>-} Buildable (Axiom (Axiom_Term (IO a))) where
1716 build (Axiom_Term _a ty) =
1717 "(_:" <> build (ty context) <> ")"
1720 -- , Buildable (Axiom a)
1721 -- , Axiomable (Axiom a)
1722 -- , Axiomable (Axiom (Axiom_Term a))
1723 ) => Axiomable (Axiom (Axiom_Term (IO a))) where
1724 axiom_type_of ctx (Axiom_Term _a ty) = ty ctx