Language/Symantic/Lib/Lambda.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE PolyKinds #-}
   4 {-# LANGUAGE UndecidableInstances #-}
   5 {-# OPTIONS_GHC -fno-warn-orphans #-}
   6 module Language.Symantic.Lib.Lambda where
   7
   8 import qualified Data.Function as Fun
   9 import qualified Data.Kind as Kind
  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.Parsing.Grammar
  18 import Language.Symantic.Typing
  19 import Language.Symantic.Compiling
  20 import Language.Symantic.Interpreting
  21 import Language.Symantic.Transforming.Trans
  22
  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         (.$) f x = trans_lift (trans_apply f .$ trans_apply x)
  35
  36         -- | Convenient 'lam' and '.$' wrapper.
  37         let_ :: term var -> (term var -> term res) -> term res
  38         let_ x y = lam y .$ x
  39
  40         id :: term a -> term a
  41         id a = lam Fun.id .$ a
  42
  43         const :: term a -> term b -> term a
  44         const a b = (lam (lam . Fun.const) .$ a) .$ b
  45
  46         -- | /Lambda composition/.
  47         (^) :: term (b -> c) -> term (a -> b) -> term (a -> c)
  48         (^) f g = lam $ \a -> f .$ (g .$ a)
  49
  50         flip :: term (a -> b -> c) -> term (b -> a -> c)
  51         flip f = lam $ \b -> lam $ \a -> (f .$ a) .$ b
  52
  53 infixr 0 .$
  54 infixr 9 ^
  55
  56 type instance Sym_of_Iface (Proxy (->)) = Sym_Lambda
  57 type instance Consts_of_Iface (Proxy (->)) = Proxy (->) ': Consts_imported_by (->)
  58 type instance Consts_imported_by (->) =
  59  [ Proxy Applicative
  60  , Proxy Functor
  61  , Proxy Monad
  62  , Proxy Monoid
  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 (Proxy @Sym_Lambda) (.$)
  96
  97 instance
  98  ( Read_TypeNameR Type_Name cs rs
  99  , Inj_Const cs (->)
 100  ) => Read_TypeNameR Type_Name cs (Proxy (->) ': rs) where
 101         read_typenameR _cs (Type_Name "(->)") k = k (ty @(->))
 102         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
 103 instance Show_Const cs => Show_Const (Proxy (->) ': cs) where
 104         show_const ConstZ{} = "(->)"
 105         show_const (ConstS c) = show_const c
 106
 107 instance -- Proj_ConC (->)
 108  ( Proj_Const cs (->)
 109  , Proj_Consts cs (Consts_imported_by (->))
 110  , Proj_Con cs
 111  ) => Proj_ConC cs (Proxy (->)) where
 112         proj_conC _ (TyConst q :$ (TyConst c :$ _r))
 113          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 114          , Just Refl <- proj_const c (Proxy @(->))
 115          = case () of
 116                  _ | Just Refl <- proj_const q (Proxy @Functor)     -> Just Con
 117                    | Just Refl <- proj_const q (Proxy @Applicative) -> Just Con
 118                    | Just Refl <- proj_const q (Proxy @Monad)       -> Just Con
 119                  _ -> Nothing
 120         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ _a :$ b))
 121          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 122          , Just Refl <- proj_const c (Proxy @(->))
 123          = case () of
 124                  _ | Just Refl <- proj_const q (Proxy @Monoid)
 125                    , Just Con  <- proj_con (t :$ b) -> Just Con
 126                  _ -> Nothing
 127         proj_conC _c _q = Nothing
 128 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy (->)))
 129 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy (->)))
 130 instance -- CompileI (->)
 131  ( Inj_Const  (Consts_of_Ifaces is) (->)
 132  , Read_TypeName Type_Name (Consts_of_Ifaces is)
 133  , Compile is
 134  ) => CompileI is (Proxy (->)) where
 135         compileI tok ctx k =
 136                 case tok of
 137                  Token_Term_Abst name_arg tok_ty_arg tok_body ->
 138                         compile_type tok_ty_arg $ \(ty_arg::Type (Consts_of_Ifaces is) h) ->
 139                         check_kind
 140                          (At Nothing SKiType)
 141                          (At (Just $ tok_ty_arg) $ kind_of ty_arg) $ \Refl ->
 142                         compileO tok_body
 143                          (LamCtx_TypeS name_arg ty_arg ctx) $
 144                          \ty_res (TermO res) ->
 145                         k (ty_arg ~> ty_res) $ TermO $
 146                          \c -> lam $ \arg ->
 147                                 res (arg `LamCtx_TermS` c)
 148                  Token_Term_App tok_lam tok_arg_actual ->
 149                         compileO tok_lam ctx $ \ty_lam (TermO lam_) ->
 150                         compileO tok_arg_actual ctx $ \ty_arg_actual (TermO arg_actual) ->
 151                         check_type2 (ty @(->)) (At (Just tok_lam) ty_lam) $ \Refl ty_arg ty_res ->
 152                         check_type
 153                          (At (Just tok_lam) ty_arg)
 154                          (At (Just tok_arg_actual) ty_arg_actual) $ \Refl ->
 155                         k ty_res $ TermO $
 156                          \c -> lam_ c .$ arg_actual c
 157                  Token_Term_Let name tok_bound tok_body ->
 158                         compileO tok_bound ctx $ \ty_bound (TermO bound) ->
 159                         compileO tok_body (LamCtx_TypeS name ty_bound ctx) $
 160                          \ty_res (TermO res) ->
 161                         k ty_res $ TermO $
 162                          \c -> let_ (bound c) $ \arg -> res (arg `LamCtx_TermS` c)
 163                  Token_Term_Var nam -> go nam ctx k
 164                         where
 165                         go :: forall meta lc ret ls rs.
 166                             Term_Name
 167                          -> LamCtx_Type is Term_Name lc
 168                          -> ( forall h.
 169                                Type (Consts_of_Ifaces is) (h::Kind.Type)
 170                             -> TermO lc h is ls rs
 171                             -> Either (Error_Term meta is) ret )
 172                          -> Either (Error_Term meta is) ret
 173                         go name lc k' =
 174                                 case lc of
 175                                  LamCtx_TypeZ -> Left $ Error_Term_unbound name
 176                                  LamCtx_TypeS n typ _ | n == name ->
 177                                         k' typ $ TermO $ \(te `LamCtx_TermS` _) -> te
 178                                  LamCtx_TypeS _n _ty lc' ->
 179                                         go name lc' $ \typ (TermO te::TermO lc' h is '[] is) ->
 180                                         k' typ $ TermO $ \(_ `LamCtx_TermS` c) -> te c
 181                  Token_Term_Compose tok_f tok_g ->
 182                  -- (.) :: (b -> c) -> (a -> b) -> a -> c
 183                         compileO tok_f ctx $ \ty_f (TermO f) ->
 184                         compileO tok_g ctx $ \ty_g (TermO g) ->
 185                         check_type2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_b ty_c ->
 186                         check_type2 (ty @(->)) (At (Just tok_g) ty_g) $ \Refl ty_a ty_g_b ->
 187                         check_type
 188                          (At (Just tok_f) ty_f_b)
 189                          (At (Just tok_g) ty_g_b) $ \Refl ->
 190                         k (ty_a ~> ty_c) $ TermO $
 191                          \c -> (^) (f c) (g c)
 192 instance
 193  Inj_Token meta ts (->) =>
 194  TokenizeT meta ts (Proxy (->)) where
 195         tokenizeT _t = mempty
 196          { tokenizers_infix = tokenizeTMod []
 197                  [ tokenize2 "." (infixR 9) Token_Term_Compose
 198                  , tokenize2 "$" (infixR 0) Token_Term_App
 199                  ]
 200          }
 201 instance Gram_Term_AtomsT meta ts (Proxy (->)) g
 202
 203 -- | The function 'Type' @(->)@,
 204 -- with an infix notation more readable.
 205 (~>) :: forall cs a b. Inj_Const cs (->)
 206  => Type cs a -> Type cs b -> Type cs (a -> b)
 207 (~>) a b = ty @(->) :$ a :$ b
 208 infixr 5 ~>