symantic-lib/Language/Symantic/Lib/Lambda.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE PolyKinds #-}
   4 {-# LANGUAGE UndecidableInstances #-}
   5 {-# OPTIONS_GHC -fno-warn-orphans #-}
   6 -- | Symantic for '(->)'.
   7 module Language.Symantic.Lib.Lambda where
   8
   9 import qualified Data.Function as Fun
  10 import Data.Monoid ((<>))
  11 import Data.Proxy (Proxy(..))
  12 import qualified Data.Text as Text
  13 import Data.Type.Equality ((:~:)(..))
  14 import Prelude hiding ((^))
  15
  16 import Language.Symantic.Parsing
  17 import Language.Symantic.Typing
  18 import Language.Symantic.Compiling
  19 import Language.Symantic.Interpreting
  20 import Language.Symantic.Transforming
  21
  22 -- * Class 'Sym_Lambda'
  23 class Sym_Lambda term where
  24         -- | /Lambda abstraction/.
  25         lam :: (term arg -> term res) -> term (arg -> res)
  26         default lam :: Trans t term => (t term arg -> t term res) -> t term (arg -> res)
  27         lam f = trans_lift $ lam $ trans_apply . f . trans_lift
  28
  29         -- | /Lambda application/.
  30         (.$) :: term (arg -> res) -> term arg -> term res
  31         default (.$) :: Trans t term => t term (arg -> res) -> t term arg -> t term res
  32         infixr 0 .$
  33         (.$) f x = trans_lift (trans_apply f .$ trans_apply x)
  34
  35         -- | Convenient 'lam' and '.$' wrapper.
  36         let_ :: term var -> (term var -> term res) -> term res
  37         let_ x y = lam y .$ x
  38
  39         id :: term a -> term a
  40         id a = lam Fun.id .$ a
  41
  42         const :: term a -> term b -> term a
  43         const a b = (lam (lam . Fun.const) .$ a) .$ b
  44
  45         -- | /Lambda composition/.
  46         (^) :: term (b -> c) -> term (a -> b) -> term (a -> c)
  47         (^) f g = lam $ \a -> f .$ (g .$ a)
  48         infixr 9 ^
  49
  50         flip :: term (a -> b -> c) -> term (b -> a -> c)
  51         flip f = lam $ \b -> lam $ \a -> (f .$ a) .$ b
  52
  53 type instance Sym_of_Iface (Proxy (->)) = Sym_Lambda
  54 type instance TyConsts_of_Iface (Proxy (->)) = Proxy (->) ': TyConsts_imported_by (->)
  55 type instance TyConsts_imported_by (->) =
  56  [ Proxy Applicative
  57  , Proxy Functor
  58  , Proxy Monad
  59  , Proxy Monoid
  60  ]
  61
  62 instance Sym_Lambda HostI where
  63         lam f = HostI (unHostI . f . HostI)
  64         (.$)  = (<*>)
  65 instance Sym_Lambda TextI where
  66         lam f = TextI $ \po v ->
  67                 let x = "x" <> Text.pack (show v) in
  68                 infix_paren po op $
  69                         "\\" <> x <> " -> " <>
  70                         unTextI (f (TextI $ \_po _v -> x)) (op, L) (succ v)
  71                 where op = infixN 1
  72         -- (.$) = textI_infix "$" (Precedence 0)
  73         (.$) (TextI a1) (TextI a2) = TextI $ \po v ->
  74                 infix_paren po op $
  75                         a1 (op, L) v <> " " <> a2 (op, R) v
  76                 where op = infixN 10
  77         let_ e in_ =
  78                 TextI $ \po v ->
  79                         let x = "x" <> Text.pack (show v) in
  80                         infix_paren po op $
  81                         "let" <> " " <> x <> " = "
  82                          <> unTextI e (infixN 0, L) (succ v) <> " in "
  83                          <> unTextI (in_ (TextI $ \_po _v -> x)) (op, L) (succ v)
  84                 where op = infixN 2
  85         (^)   = textI_infix "." (infixR 9)
  86         id    = textI1 "id"
  87         const = textI2 "const"
  88         flip  = textI1 "flip"
  89 instance (Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (DupI r1 r2) where
  90         lam f = dupI_1 lam_f `DupI` dupI_2 lam_f
  91                 where lam_f = lam f
  92         (.$) = dupI2 @Sym_Lambda (.$)
  93
  94 instance
  95  ( Read_TyNameR TyName cs rs
  96  , Inj_TyConst cs (->)
  97  ) => Read_TyNameR TyName cs (Proxy (->) ': rs) where
  98         read_TyNameR _cs (TyName "(->)") k = k (ty @(->))
  99         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
 100 instance Show_TyConst cs => Show_TyConst (Proxy (->) ': cs) where
 101         show_TyConst TyConstZ{} = "(->)"
 102         show_TyConst (TyConstS c) = show_TyConst c
 103
 104 instance -- Proj_TyConC (->)
 105  ( Proj_TyConst cs (->)
 106  , Proj_TyConsts cs (TyConsts_imported_by (->))
 107  , Proj_TyCon cs
 108  ) => Proj_TyConC cs (Proxy (->)) where
 109         proj_TyConC _ (TyConst q :$ (TyConst c :$ _r))
 110          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 111          , Just Refl <- proj_TyConst c (Proxy @(->))
 112          = case () of
 113                  _ | Just Refl <- proj_TyConst q (Proxy @Functor)     -> Just TyCon
 114                    | Just Refl <- proj_TyConst q (Proxy @Applicative) -> Just TyCon
 115                    | Just Refl <- proj_TyConst q (Proxy @Monad)       -> Just TyCon
 116                  _ -> Nothing
 117         proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ _a :$ b))
 118          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 119          , Just Refl <- proj_TyConst c (Proxy @(->))
 120          = case () of
 121                  _ | Just Refl <- proj_TyConst q (Proxy @Monoid)
 122                    , Just TyCon  <- proj_TyCon (t :$ b) -> Just TyCon
 123                  _ -> Nothing
 124         proj_TyConC _c _q = Nothing
 125 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy (->)))
 126 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy (->)))
 127 instance -- CompileI (->)
 128  ( Inj_TyConst cs (->)
 129  , Read_TyName TyName cs
 130  , Compile cs is
 131  ) => CompileI cs is (Proxy (->)) where
 132         compileI tok ctx k =
 133                 case tok of
 134                  Token_Term_Abst name_arg tok_ty_arg tok_body ->
 135                         compile_Type tok_ty_arg $ \(ty_arg::Type cs h) ->
 136                         check_Kind
 137                          (At Nothing SKiType)
 138                          (At (Just $ tok_ty_arg) $ kind_of ty_arg) $ \Refl ->
 139                         compileO tok_body
 140                          (TyCtxS name_arg ty_arg ctx) $
 141                          \ty_res (TermO res) ->
 142                         k (ty_arg ~> ty_res) $ TermO $
 143                          \c -> lam $ \arg ->
 144                                 res (arg `TeCtxS` c)
 145                  Token_Term_App tok_lam tok_arg_actual ->
 146                         compileO tok_lam ctx $ \ty_lam (TermO lam_) ->
 147                         compileO tok_arg_actual ctx $ \ty_arg_actual (TermO arg_actual) ->
 148                         check_TyEq2 (ty @(->)) (At (Just tok_lam) ty_lam) $ \Refl ty_arg ty_res ->
 149                         check_TyEq
 150                          (At (Just tok_lam) ty_arg)
 151                          (At (Just tok_arg_actual) ty_arg_actual) $ \Refl ->
 152                         k ty_res $ TermO $
 153                          \c -> lam_ c .$ arg_actual c
 154                  Token_Term_Let name tok_bound tok_body ->
 155                         compileO tok_bound ctx $ \ty_bound (TermO bound) ->
 156                         compileO tok_body (TyCtxS name ty_bound ctx) $ \ty_res (TermO res) ->
 157                         k ty_res $ TermO $
 158                          \c -> let_ (bound c) $ \arg -> res (arg `TeCtxS` c)
 159                  Token_Term_Var nam -> go nam ctx k
 160                         where
 161                         go :: forall meta lc ret ls rs.
 162                             TeName
 163                          -> TyCtx TeName cs lc
 164                          -> ( forall h.
 165                                Type cs (h:: *)
 166                             -> TermO lc h is ls rs
 167                             -> Either (Error_Term meta cs is) ret )
 168                          -> Either (Error_Term meta cs is) ret
 169                         go name lc k' =
 170                                 case lc of
 171                                  TyCtxZ -> Left $ Error_Term_unbound name
 172                                  TyCtxS n typ _ | n == name ->
 173                                         k' typ $ TermO $ \(te `TeCtxS` _) -> te
 174                                  TyCtxS _n _ty lc' ->
 175                                         go name lc' $ \typ (TermO te::TermO lc' h is '[] is) ->
 176                                         k' typ $ TermO $ \(_ `TeCtxS` c) -> te c
 177                  Token_Term_Compose tok_f tok_g ->
 178                  -- (.) :: (b -> c) -> (a -> b) -> a -> c
 179                         compileO tok_f ctx $ \ty_f (TermO f) ->
 180                         compileO tok_g ctx $ \ty_g (TermO g) ->
 181                         check_TyEq2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_b ty_c ->
 182                         check_TyEq2 (ty @(->)) (At (Just tok_g) ty_g) $ \Refl ty_a ty_g_b ->
 183                         check_TyEq
 184                          (At (Just tok_f) ty_f_b)
 185                          (At (Just tok_g) ty_g_b) $ \Refl ->
 186                         k (ty_a ~> ty_c) $ TermO $
 187                          \c -> (^) (f c) (g c)
 188 instance
 189  Inj_Token meta ts (->) =>
 190  TokenizeT meta ts (Proxy (->)) where
 191         tokenizeT _t = mempty
 192          { tokenizers_infix = tokenizeTMod []
 193                  [ tokenize2 "." (infixR 9) Token_Term_Compose
 194                  , tokenize2 "$" (infixR 0) Token_Term_App
 195                  ]
 196          }
 197 instance Gram_Term_AtomsT meta ts (Proxy (->)) g
 198
 199 -- | The function 'Type' @(->)@,
 200 -- with an infix notation more readable.
 201 (~>) :: forall cs a b. Inj_TyConst cs (->)
 202  => Type cs a -> Type cs b -> Type cs (a -> b)
 203 (~>) a b = ty @(->) :$ a :$ b
 204 infixr 5 ~>