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