Language/Symantic/Compiling/Term.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE DataKinds #-}
   3 {-# LANGUAGE DefaultSignatures #-}
   4 {-# LANGUAGE FlexibleContexts #-}
   5 {-# LANGUAGE FlexibleInstances #-}
   6 {-# LANGUAGE GADTs #-}
   7 {-# LANGUAGE KindSignatures #-}
   8 {-# LANGUAGE MultiParamTypeClasses #-}
   9 {-# LANGUAGE OverloadedStrings #-}
  10 {-# LANGUAGE PolyKinds #-}
  11 {-# LANGUAGE Rank2Types #-}
  12 {-# LANGUAGE ScopedTypeVariables #-}
  13 {-# LANGUAGE StandaloneDeriving #-}
  14 {-# LANGUAGE TypeFamilies #-}
  15 {-# LANGUAGE TypeInType #-}
  16 {-# LANGUAGE TypeOperators #-}
  17 {-# LANGUAGE UndecidableInstances #-}
  18 {-# OPTIONS_GHC -fno-warn-orphans #-}
  19 module Language.Symantic.Compiling.Term where
  20
  21 import qualified Data.Function as Fun
  22 import qualified Data.Kind as Kind
  23 import Data.Kind hiding (Type)
  24 import Data.Monoid ((<>))
  25 import Data.Proxy (Proxy(..))
  26 import Data.String (IsString)
  27 import Data.Text (Text)
  28 import qualified Data.Text as Text
  29 import Data.Type.Equality ((:~:)(..))
  30 import GHC.Exts (Constraint)
  31 import Prelude hiding (not)
  32
  33 import Language.Symantic.Lib.Data.Type.List
  34 import Language.Symantic.Typing
  35 import Language.Symantic.Interpreting
  36 import Language.Symantic.Transforming.Trans
  37
  38 -- * Type 'Term'
  39 -- | 'TermLC' applied on a 'LamCtx_Type'.
  40 data Term is h
  41  =   Term
  42  (forall term. ( Sym_of_Ifaces is term
  43                , Sym_Lambda term
  44                ) => term h)
  45
  46 -- ** Type 'TermLC'
  47 -- | A data type embedding a universal quantification
  48 -- over an interpreter @term@
  49 -- and qualified by the symantics of a term.
  50 --
  51 -- Moreover the term is abstracted by a 'LamCtx_Term'
  52 -- built top-down at parsing time
  53 -- to build a /Higher-Order Abstract Syntax/ (HOAS)
  54 -- for /lambda abstractions/ ('lam').
  55 --
  56 -- This data type is used to keep a parsed term polymorphic enough
  57 -- to stay interpretable by different interpreters.
  58 --
  59 -- * @(@'Sym_of_Ifaces'@ is term)@
  60 -- is needed when a symantic method includes a polymorphic type
  61 -- and thus calls: 'term_from'.
  62 --
  63 -- * @(@'Sym_of_Ifaces'@ ls term)@ and @(@'Sym_of_Ifaces'@ rs term)@
  64 -- are needed to be able to write the instance:
  65 -- @(@'Term_fromR'@ is ls (i ': rs) ast)@.
  66 --
  67 -- * @(@'Sym_Lambda'@ term)@
  68 -- is needed to be able to parse partially applied functions
  69 -- (when their type is knowable).
  70 data TermLC ctx h is ls rs
  71  =   TermLC
  72  (forall term. ( Sym_of_Ifaces is term
  73                , Sym_of_Ifaces ls term
  74                , Sym_of_Ifaces rs term
  75                , Sym_Lambda term
  76                ) => LamCtx_Term term ctx -> term h)
  77
  78 -- * Type 'ETerm'
  79 -- | Existential 'Term', with its 'Type'.
  80 data ETerm is
  81  = forall (h::Kind.Type). ETerm
  82    (Type (Consts_of_Ifaces is) h)
  83    (Term is h)
  84
  85 -- | Like 'term_from' but for a term with an empty /lambda context/.
  86 root_term_from
  87  :: Term_from is ast
  88  => ast -> Either (Error_Term is ast) (ETerm is)
  89 root_term_from ast =
  90         term_from ast LamCtx_TypeZ $ \ty (TermLC te) ->
  91         Right $ ETerm ty $ Term $ te LamCtx_TermZ
  92
  93 -- * Type 'Term_from'
  94 -- | Convenient type synonym wrapping 'Term_fromR'
  95 -- to initiate its recursion.
  96 class Term_from is ast where
  97         term_from :: Term_fromT ast ctx ret is '[] is
  98 instance
  99  ( AST ast
 100  , Eq (Lexem ast)
 101  , Term_fromR is '[] is ast
 102  ) => Term_from is ast where
 103         term_from ast ctx k =
 104                 case replace_var (ast_lexem ast) ctx k of
 105                  Left Error_Term_unsupported -> term_fromR ast ctx k
 106                  x -> x
 107                 where
 108                 replace_var
 109                  :: forall lc ret.
 110                     Lexem ast
 111                  -> LamCtx_Type is (Lexem ast) lc
 112                  -> ( forall h.
 113                        Type (Consts_of_Ifaces is) (h::Kind.Type)
 114                     -> TermLC lc h is '[] is
 115                     -> Either (Error_Term is ast) ret )
 116                  -> Either (Error_Term is ast) ret
 117                 replace_var name lc k' =
 118                         case lc of
 119                          LamCtx_TypeZ -> Left $ Error_Term_unsupported
 120                          LamCtx_TypeS n ty _ | n == name ->
 121                                 k' ty $ TermLC $ \(te `LamCtx_TermS` _) -> te
 122                          LamCtx_TypeS _n _ty lc' ->
 123                                 replace_var name lc' $ \ty (TermLC te::TermLC lc' h is '[] is) ->
 124                                 k' ty $ TermLC $ \(_ `LamCtx_TermS` c) -> te c
 125
 126 -- ** Type 'Term_fromT'
 127 -- | Convenient type synonym defining a term parser.
 128 type Term_fromT ast ctx ret is ls rs
 129  = ast
 130  -> LamCtx_Type is (Lexem ast) ctx
 131  -- ^ The bound variables in scope and their types:
 132  -- built top-down in the heterogeneous list @ctx@,
 133  -- from the closest including /lambda abstraction/ to the farest.
 134  -> ( forall h.
 135        Type (Consts_of_Ifaces is) (h::Kind.Type)
 136     -> TermLC ctx h is ls rs
 137     -> Either (Error_Term is ast) ret )
 138  -- ^ The accumulating continuation called bottom-up.
 139  -> Either (Error_Term is ast) ret
 140
 141 -- ** Type 'Term_fromIT'
 142 -- | Almost like 'Term_fromT', but with the remaining 'ast_nodes'
 143 -- given to the continuation so that 'term_apply' can be used within
 144 -- the instance 'Term_fromR'@ is ls (i ': rs) ast@.
 145 type Term_fromIT ast ctx ret is ls rs
 146  = ast
 147  -> LamCtx_Type is (Lexem ast) ctx
 148  -> ( forall h.
 149        [ast]
 150     -> Type (Consts_of_Ifaces is) (h::Kind.Type)
 151     -> TermLC ctx h is ls rs
 152     -> Either (Error_Term is ast) ret )
 153  -> Either (Error_Term is ast) ret
 154
 155 -- ** Class 'Term_fromR'
 156 -- | Intermediate type class to construct an instance of 'Term_from'
 157 -- from many instances of 'Term_fromI', one for each item of @is@.
 158 --
 159 -- * @is@: starting  list of /term constants/.
 160 -- * @ls@: done      list of /term constants/.
 161 -- * @rs@: remaining list of /term constants/.
 162 class Term_fromR (is::[*]) (ls::[*]) (rs::[*]) ast where
 163         term_fromR :: Term_fromT ast ctx ret is ls rs
 164         default term_fromR :: AST ast => Term_fromT ast ctx ret is ls rs
 165         term_fromR ast _ctx _k =
 166                 Left $ Error_Term_unknown $
 167                 At (Just ast) $ ast_lexem ast
 168
 169 -- | Test whether @i@ handles the work of 'Term_from' or not,
 170 -- or recurse on @rs@, preserving the starting list of /term constants/,
 171 -- and keeping a list of those done to construct 'TermLC'.
 172 instance
 173  ( Term_fromI is i ast
 174  , Term_fromR is (i ': ls) rs ast
 175  , Term_from is ast
 176  , Inj_Const (Consts_of_Ifaces is) (->)
 177  ) => Term_fromR is ls (i ': rs) ast where
 178         term_fromR ast ctx k =
 179                 case term_fromI ast ctx $ \as ty (TermLC te
 180                  ::TermLC ctx h is ls (i ': rs)) ->
 181                         term_apply ast as ctx ty (TermLC te) k of
 182                  Left Error_Term_unsupported ->
 183                         term_fromR ast ctx $ \ty (TermLC te
 184                          ::TermLC ctx h is (i ': ls) rs) ->
 185                                 k ty (TermLC te
 186                                  ::TermLC ctx h is ls (i ': rs))
 187                  x -> x
 188 -- | End the recursion.
 189 instance AST ast => Term_fromR is ls '[] ast
 190
 191 -- | Apply the given @ast@s to the given 'TermLC',
 192 -- or return an 'Error_Term'.
 193 term_apply ::
 194  ( Term_from is ast
 195  , Inj_Const (Consts_of_Ifaces is) (->)
 196  ) => ast -> [ast]
 197  -> LamCtx_Type is (Lexem ast) ctx
 198  -> Type (Consts_of_Ifaces is) (h::Kind.Type)
 199  -> TermLC ctx h is ls rs
 200  -> ( forall h'.
 201        Type (Consts_of_Ifaces is) (h' ::Kind.Type)
 202     -> TermLC ctx h' is ls rs
 203     -> Either (Error_Term is ast) ret )
 204  -> Either (Error_Term is ast) ret
 205 term_apply ast_f args ctx ty_f te_f@(TermLC f) k =
 206         case args of
 207          [] -> k ty_f te_f
 208          ast_a:as ->
 209                 term_from ast_a ctx $ \ty_a (TermLC a) ->
 210                 check_type2 tyFun ast_f ty_f $ \Refl ty_arg ty_res ->
 211                 check_type (At (Just ast_f) ty_arg) (At (Just ast_a) ty_a) $ \Refl ->
 212                 term_apply ast_f as ctx ty_res (TermLC $ \c -> f c .$ a c) k
 213
 214 -- ** Class 'Term_fromI'
 215 -- | Handle the work of 'Term_from' for a given /interface/ @i@,
 216 -- that is: maybe it handles the given /interface/,
 217 -- and if so, maybe the term can be parsed.
 218 class Term_fromI (is::[*]) (i:: *) ast where
 219         term_fromI :: Term_fromIT ast ctx ret is ls (i ': rs)
 220         term_fromI _ast _ctx _k = Left $ Error_Term_unsupported
 221
 222 -- * Type family 'Sym_of_Ifaces'
 223 type family Sym_of_Ifaces (is::[*]) (term:: * -> *) :: Constraint where
 224         Sym_of_Ifaces '[] term = ()
 225         Sym_of_Ifaces (i ': is) term = (Sym_of_Iface i term, Sym_of_Ifaces is term)
 226
 227 -- ** Type family 'Sym_of_Iface'
 228 type family Sym_of_Iface (i:: *) :: {-term-}(* -> *) -> Constraint
 229
 230 -- * Type 'Consts_of_Ifaces'
 231 type Consts_of_Ifaces is = Nub (Consts_of_IfaceR is)
 232
 233 -- ** Type family 'Consts_of_IfaceR'
 234 type family Consts_of_IfaceR (is::[*]) where
 235         Consts_of_IfaceR '[] = '[]
 236         Consts_of_IfaceR (i ': is) = Consts_of_Iface i ++ Consts_of_IfaceR is
 237
 238 -- ** Type family 'Consts_of_Iface'
 239 type family   Consts_of_Iface (i::k) :: [*]
 240 type instance Consts_of_Iface (Proxy Enum) = Proxy Enum ': Consts_imported_by Enum
 241
 242 -- * Type 'LamCtx_Type'
 243 -- | GADT for a typing context,
 244 -- accumulating an @item@ at each lambda;
 245 -- used to accumulate object-types (in 'Expr_From')
 246 -- or host-terms (in 'HostI')
 247 -- associated with the 'LamVar's in scope.
 248 data LamCtx_Type (is::[*]) (name:: *) (ctx::[*]) where
 249         LamCtx_TypeZ :: LamCtx_Type is name '[]
 250         LamCtx_TypeS :: name
 251                      -> Type (Consts_of_Ifaces is) (h::Kind.Type)
 252                      -> LamCtx_Type is name hs
 253                      -> LamCtx_Type is name (h ': hs)
 254 infixr 5 `LamCtx_TypeS`
 255
 256 -- ** Type 'LamVarName'
 257 type LamVarName = Text
 258
 259 -- * Type 'LamCtx_Term'
 260 data LamCtx_Term (term:: * -> *) (ctx::[*]) where
 261         LamCtx_TermZ :: LamCtx_Term term '[]
 262         LamCtx_TermS :: term h
 263                      -> LamCtx_Term term hs
 264                      -> LamCtx_Term term (h ': hs)
 265 infixr 5 `LamCtx_TermS`
 266
 267 -- * Type 'Error_Term'
 268 data Error_Term (is::[*]) ast
 269  =   Error_Term_unknown (At ast (Lexem ast))
 270  |   Error_Term_unsupported
 271  |   Error_Term_Syntax (Error_Syntax ast)
 272  |   Error_Term_Constraint_not_deductible (At ast (KType (Consts_of_Ifaces is) Constraint))
 273  |   Error_Term_Family_instance_missing (At ast ())
 274  |   Error_Term_Typing (At ast (Error_Type (Consts_of_Ifaces is) ast))
 275  |   Error_Term_Type_mismatch (At ast (EType (Consts_of_Ifaces is)))
 276                               (At ast (EType (Consts_of_Ifaces is)))
 277  |   Error_Term_Type_is_not_an_application (At ast (EType (Consts_of_Ifaces is)))
 278 deriving instance (Eq ast, Eq (Lexem ast)) => Eq (Error_Term is ast)
 279 deriving instance (Show ast, Show (Lexem ast), Show_Const (Consts_of_Ifaces is)) => Show (Error_Term is ast)
 280
 281 instance Lift_Error_Syntax (Error_Term is) where
 282         lift_error_syntax = Error_Term_Syntax
 283
 284 -- ** Checks
 285
 286 -- | Check that the 'kind_of' a given 'Type's equals a given kind,
 287 -- or fail with 'Error_Type_Kind_mismatch'.
 288 check_kind
 289  :: ast -> SKind k
 290  -> At ast (Type (Consts_of_Ifaces is) (t::kt))
 291  -> ((k :~: kt) -> Either (Error_Term is ast) ret)
 292  -> Either (Error_Term is ast) ret
 293 check_kind ast ki (At at_ty ty) k =
 294         let ki_ty = kind_of ty in
 295         case eq_skind ki ki_ty of
 296          Just Refl -> k Refl
 297          Nothing -> Left $ Error_Term_Typing $
 298                 At (Just ast) $
 299                 Error_Type_Kind_mismatch
 300                  (At Nothing $ EKind SKiType)
 301                  (At at_ty $ EKind ki_ty)
 302
 303 -- | Check that a given 'Type' is a /type application/,
 304 -- or fail with 'Error_Term_Type_is_not_an_application'.
 305 check_app
 306  :: ast -> Type (Consts_of_Ifaces is) (fx::kfx)
 307  -> (forall kx f x. (fx :~: f x)
 308   -> Type (Consts_of_Ifaces is) (f::kx -> kfx)
 309   -> Type (Consts_of_Ifaces is) (x::kx)
 310   -> Either (Error_Term is ast) ret)
 311  -> Either (Error_Term is ast) ret
 312 check_app ast ty_fx k =
 313         case ty_fx of
 314          ty_f :$ ty_x -> k Refl ty_f ty_x
 315          _ -> Left $ Error_Term_Type_is_not_an_application $
 316                 At (Just ast) $ EType ty_fx
 317
 318 -- | Check that two given 'Type's are equal,
 319 -- or fail with 'Error_Term_Type_mismatch'.
 320 check_type
 321  :: At ast (Type (Consts_of_Ifaces is) x)
 322  -> At ast (Type (Consts_of_Ifaces is) y)
 323  -> ((x :~: y) -> Either (Error_Term is ast) ret)
 324  -> Either (Error_Term is ast) ret
 325 check_type (At at_x x) (At at_y y) k =
 326         case eq_type x y of
 327          Just Refl -> k Refl
 328          Nothing -> Left $ Error_Term_Type_mismatch
 329                  (At at_x $ EType x)
 330                  (At at_y $ EType y)
 331
 332 -- | Convenient wrapper to check for a 'Type' of kind: @* -> *@.
 333 check_type1
 334  :: Type (Consts_of_Ifaces is) ty
 335  -> ast
 336  -> Type (Consts_of_Ifaces is) (fx:: *)
 337  -> (forall x. (fx :~: ty x)
 338   -> Type (Consts_of_Ifaces is) (x:: *)
 339   -> Either (Error_Term is ast) ret)
 340  -> Either (Error_Term is ast) ret
 341 check_type1 ty ast_ta ty_ta k =
 342         check_app ast_ta ty_ta $ \Refl ty_ta_t ty_ta_a ->
 343         check_kind ast_ta (SKiType `SKiArrow` SKiType) (At (Just ast_ta) ty_ta_t) $ \Refl ->
 344         check_type (At Nothing ty) (At (Just ast_ta) ty_ta_t) $ \Refl ->
 345         k Refl ty_ta_a
 346
 347 -- | Convenient wrapper to check for a 'Type' of kind: @* -> * -> *@.
 348 check_type2
 349  :: Type (Consts_of_Ifaces is) (ty:: * -> * -> *)
 350  -> ast -> Type (Consts_of_Ifaces is) a2b
 351  -> (forall a b. (a2b :~: (ty a b))
 352   -> Type (Consts_of_Ifaces is) a
 353   -> Type (Consts_of_Ifaces is) b
 354   -> Either (Error_Term is ast) ret)
 355  -> Either (Error_Term is ast) ret
 356 check_type2 ty ast ty_a2b k =
 357         check_app ast ty_a2b $ \Refl ty_a2b_a2 ty_a2b_b ->
 358         check_app ast ty_a2b_a2 $ \Refl ty_a2b_ty ty_a2b_a ->
 359         check_kind ast (SKiType `SKiArrow` SKiType `SKiArrow` SKiType) (At (Just ast) ty_a2b_ty) $ \Refl ->
 360         check_type (At Nothing ty) (At (Just ast) ty_a2b_ty) $ \Refl ->
 361         k Refl ty_a2b_a ty_a2b_b
 362
 363 -- | Check that a given 'Constraint' holds,
 364 -- or fail with 'Error_Term_Constraint_not_deductible'.
 365 check_constraint
 366  :: Proj_Con (Consts_of_Ifaces is)
 367  => At ast (Type (Consts_of_Ifaces is) (q::Constraint))
 368  -> (Con q -> Either (Error_Term is ast) ret)
 369  -> Either (Error_Term is ast) ret
 370 check_constraint (At at_q q) k =
 371         case proj_con q of
 372          Just Con -> k Con
 373          Nothing -> Left $ Error_Term_Constraint_not_deductible $
 374                 At at_q $ KType q
 375
 376 -- | Convenient wrapper to check for a 'Constraint'
 377 -- over a 'Type' of kind: @* -> *@.
 378 check_constraint1
 379  :: Proj_Con (Consts_of_Ifaces is)
 380  => Type (Consts_of_Ifaces is) con
 381  -> ast -> Type (Consts_of_Ifaces is) (fx:: *)
 382  -> (forall f x. (fx :~: f x)
 383   -> Con (con f)
 384   -> Type (Consts_of_Ifaces is) (f:: * -> *)
 385   -> Type (Consts_of_Ifaces is) (x:: *)
 386   -> Either (Error_Term is ast) ret)
 387  -> Either (Error_Term is ast) ret
 388 check_constraint1 con ast_ta ty_ta k =
 389         check_app ast_ta ty_ta $ \Refl ty_ta_t ty_ta_a ->
 390         check_kind ast_ta (SKiType `SKiArrow` SKiType) (At (Just ast_ta) ty_ta_t) $ \Refl ->
 391         check_constraint (At (Just ast_ta) (con :$ ty_ta_t)) $ \Con ->
 392         k Refl Con ty_ta_t ty_ta_a
 393
 394 -- | Check that a given /type family/ is supported,
 395 -- or fail with 'Error_Term_Family_instance_missing'.
 396 check_family
 397  :: Proj_Fam (Consts_of_Ifaces is) fam
 398  => Proxy fam
 399  -> At ast (Type (Consts_of_Ifaces is) h)
 400  -> (Type (Consts_of_Ifaces is) (Fam fam h) -> Either (Error_Term is ast) ret)
 401  -> Either (Error_Term is ast) ret
 402 check_family fam (At at_ty ty) k =
 403         case proj_fam fam ty of
 404          Just t -> k t
 405          Nothing -> Left $ Error_Term_Family_instance_missing $
 406                 At at_ty ()
 407
 408 -- * Class 'Sym_Lambda'
 409 class Sym_Lambda term where
 410         -- | /Lambda abstraction/.
 411         lam :: (term arg -> term res) -> term ((->) arg res)
 412         default lam :: Trans t term
 413          => (t term arg -> t term res)
 414          -> t term ((->) arg res)
 415         lam f = trans_lift $ lam $ trans_apply . f . trans_lift
 416
 417         -- | /Lambda application/.
 418         (.$) :: term ((->) arg res) -> term arg -> term res
 419         default (.$) :: Trans t term
 420          => t term ((->) arg res) -> t term arg -> t term res
 421         (.$) f x = trans_lift (trans_apply f .$ trans_apply x)
 422
 423         -- | Convenient 'lam' and '.$' wrapper.
 424         let_ :: term var -> (term var -> term res) -> term res
 425         let_ x y = lam y .$ x
 426
 427         id :: term a -> term a
 428         id a = lam Fun.id .$ a
 429
 430         const :: term a -> term b -> term a
 431         const a b = lam (lam . Fun.const) .$ a .$ b
 432
 433         -- | /Lambda composition/.
 434         (#) :: term (b -> c) -> term (a -> b) -> term (a -> c)
 435         (#) f g = lam $ \a -> f .$ (g .$ a)
 436
 437         flip :: term (a -> b -> c) -> term (b -> a -> c)
 438         flip f = lam $ \b -> lam $ \a -> f .$ a .$ b
 439
 440 infixl 0 .$
 441 infixr 9 #
 442
 443 type instance Sym_of_Iface (Proxy (->)) = Sym_Lambda
 444 type instance Consts_of_Iface (Proxy (->)) = Proxy (->) ': Consts_imported_by (->)
 445 type instance Consts_imported_by (->) =
 446  [ Proxy Applicative
 447  , Proxy Functor
 448  , Proxy Monad
 449  , Proxy Monoid
 450  ]
 451
 452 instance Sym_Lambda HostI where
 453         lam f = HostI (unHostI . f . HostI)
 454         (.$)  = (<*>)
 455 instance Sym_Lambda TextI where
 456         lam f = TextI $ \p v ->
 457                 let p' = Precedence 1 in
 458                 let x = "x" <> Text.pack (show v) in
 459                 paren p p' $ "\\" <> x <> " -> "
 460                  <> unTextI (f (TextI $ \_p _v -> x)) p' (succ v)
 461         -- (.$) = textI_infix "$" (Precedence 0)
 462         (.$) (TextI a1) (TextI a2) =
 463                 TextI $ \p v ->
 464                         let p' = precedence_App in
 465                         paren p p' $ a1 p' v <> " " <> a2 p' v
 466         let_ e in_ =
 467                 TextI $ \p v ->
 468                         let p' = Precedence 2 in
 469                         let x = "x" <> Text.pack (show v) in
 470                         paren p p' $ "let" <> " " <> x <> " = "
 471                          <> unTextI e (Precedence 0) (succ v) <> " in "
 472                          <> unTextI (in_ (TextI $ \_p _v -> x)) p' (succ v)
 473         (#)   = textI_infix "." (Precedence 9)
 474         id    = textI_app1 "id"
 475         const = textI_app2 "const"
 476         flip  = textI_app1 "flip"
 477 instance (Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (DupI r1 r2) where
 478         lam f = dupI_1 lam_f `DupI` dupI_2 lam_f
 479                 where lam_f = lam f
 480         (.$) = dupI2 (Proxy::Proxy Sym_Lambda) (.$)
 481
 482 instance Const_from Text cs => Const_from Text (Proxy (->) ': cs) where
 483         const_from "(->)" k = k (ConstZ kind)
 484         const_from s k = const_from s $ k . ConstS
 485 instance Show_Const cs => Show_Const (Proxy (->) ': cs) where
 486         show_const ConstZ{} = "(->)"
 487         show_const (ConstS c) = show_const c
 488
 489 instance -- Proj_ConC (->)
 490  ( Proj_Const cs (->)
 491  , Proj_Consts cs (Consts_imported_by (->))
 492  , Proj_Con cs
 493  ) => Proj_ConC cs (Proxy (->)) where
 494         proj_conC _ (TyConst q :$ (TyConst c :$ _r))
 495          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 496          , Just Refl <- proj_const c (Proxy::Proxy (->))
 497          = case () of
 498                  _ | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
 499                    | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
 500                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
 501                  _ -> Nothing
 502         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ _a :$ b))
 503          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 504          , Just Refl <- proj_const c (Proxy::Proxy (->))
 505          = case () of
 506                  _ | Just Refl <- proj_const q (Proxy::Proxy Monoid)
 507                    , Just Con  <- proj_con (t :$ b) -> Just Con
 508                  _ -> Nothing
 509         proj_conC _c _q = Nothing
 510 instance -- Term_fromI (->)
 511  ( AST ast
 512  , Lexem ast ~ LamVarName
 513  , Inj_Const  (Consts_of_Ifaces is) (->)
 514  , Const_from (Lexem ast) (Consts_of_Ifaces is)
 515  , Term_from is ast
 516  ) => Term_fromI is (Proxy (->)) ast where
 517         term_fromI ast ctx k =
 518                 case ast_lexem ast of
 519                  "\\" -> -- lambda abstration
 520                         from_ast3 ast $ \ast_name ast_ty_arg ast_body as ->
 521                         either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
 522                         type_from ast_ty_arg $ \ty_arg -> Right $
 523                         check_kind ast SKiType (At (Just ast) ty_arg) $ \Refl ->
 524                         term_from ast_body
 525                          (LamCtx_TypeS (ast_lexem ast_name) ty_arg ctx) $
 526                          \ty_res (TermLC res) ->
 527                         k as (ty_arg ~> ty_res) $ TermLC $
 528                          \c -> lam $ \arg ->
 529                                 res (arg `LamCtx_TermS` c)
 530                  " " -> -- lambda application
 531                         from_ast2 ast $ \ast_lam ast_arg_actual as ->
 532                         term_from ast_lam ctx $ \ty_lam (TermLC lam_) ->
 533                         term_from ast_arg_actual ctx $ \ty_arg_actual (TermLC arg_actual) ->
 534                         check_type2 tyFun ast_lam ty_lam $ \Refl ty_arg ty_res ->
 535                         check_type
 536                          (At (Just ast_lam) ty_arg)
 537                          (At (Just ast_arg_actual) ty_arg_actual) $ \Refl ->
 538                         k as ty_res $ TermLC $
 539                          \c -> lam_ c .$ arg_actual c
 540                  "let" ->
 541                         from_ast3 ast $ \ast_name ast_bound ast_body as ->
 542                         term_from ast_bound ctx $ \ty_bound (TermLC bound) ->
 543                         term_from ast_body (LamCtx_TypeS (ast_lexem ast_name) ty_bound ctx) $
 544                          \ty_res (TermLC res) ->
 545                         k as ty_res $ TermLC $
 546                          \c -> let_ (bound c) $ \arg -> res (arg `LamCtx_TermS` c)
 547                  _ -> Left $ Error_Term_unsupported
 548
 549 -- | The '(->)' 'Type'
 550 tyFun :: Inj_Const cs (->) => Type cs (->)
 551 tyFun = TyConst inj_const
 552
 553 -- | The function 'Type' @(->)@,
 554 -- with an infix notation more readable.
 555 (~>) :: forall cs a b. Inj_Const cs (->)
 556  => Type cs a -> Type cs b -> Type cs (a -> b)
 557 (~>) a b = tyFun :$ a :$ b
 558 infixr 5 ~>
 559
 560 syFun :: IsString a => [Syntax a] -> Syntax a
 561 syFun = Syntax "(->)"
 562
 563 (.>) :: IsString a => Syntax a -> Syntax a -> Syntax a
 564 a .> b = syFun [a, b]
 565 infixr 3 .>
 566
 567 syLam :: IsString a => Syntax a -> Syntax a -> Syntax a -> Syntax a
 568 syLam arg ty body = Syntax "\\" [arg, ty, body]
 569
 570 syApp :: IsString a => Syntax a -> Syntax a -> Syntax a
 571 syApp lam_ arg = Syntax " " [lam_, arg]
 572 infixl 0 `syApp`
 573
 574 syLet :: IsString a => Syntax a -> Syntax a -> Syntax a -> Syntax a
 575 syLet name bound body = Syntax "let" [name, bound, body]
 576
 577 {-
 578 -- * Checks
 579
 580 -- | Parsing utility to check that the type resulting
 581 -- from the application of a given type family to a given type
 582 -- is within the type stack,
 583 -- or raise 'Error_Term_Type_mismatch'.
 584 check_type0_family
 585  :: forall ast is tf root ty h ret.
 586  ( root ~ Root_of_Expr is
 587  , ty ~ Type_Root_of_Expr is
 588  , Type0_Family tf ty
 589  , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
 590                    (Error_of_Expr ast root)
 591  ) => Proxy tf -> Proxy is -> ast -> ty h
 592  -> (ty (Host_of_Type0_Family tf h) -> Either (Error_of_Expr ast root) ret)
 593  -> Either (Error_of_Expr ast root) ret
 594 check_type0_family tf is ast ty k =
 595         case type0_family tf ty of
 596          Just t -> k t
 597          Nothing -> Left $ error_expr is $
 598                 Error_Term_Type (error_type_lift $ Error_Type_No_Type_Family ast) ast
 599
 600 -}