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.Typing
  18 import Language.Symantic.Compiling
  19 import Language.Symantic.Interpreting
  20 import Language.Symantic.Transforming
  21
  22
  23 -- * Class 'Sym_Lambda'
  24 class Sym_Lambda term where
  25         -- | /Lambda abstraction/.
  26         lam :: (term arg -> term res) -> term (arg -> res)
  27         default lam :: Trans t term => (t term arg -> t term res) -> t term (arg -> res)
  28         lam f = trans_lift $ lam $ trans_apply . f . trans_lift
  29
  30         -- | /Lambda application/.
  31         (.$) :: term (arg -> res) -> term arg -> term res
  32         default (.$) :: Trans t term => t term (arg -> res) -> t term arg -> t term res
  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
  49         flip :: term (a -> b -> c) -> term (b -> a -> c)
  50         flip f = lam $ \b -> lam $ \a -> (f .$ a) .$ b
  51
  52 infixr 0 .$
  53 infixr 9 ^
  54
  55 type instance Sym_of_Iface (Proxy (->)) = Sym_Lambda
  56 type instance Consts_of_Iface (Proxy (->)) = Proxy (->) ': Consts_imported_by (->)
  57 type instance Consts_imported_by (->) =
  58  [ Proxy Applicative
  59  , Proxy Functor
  60  , Proxy Monad
  61  , Proxy Monoid
  62  ]
  63
  64 instance Sym_Lambda HostI where
  65         lam f = HostI (unHostI . f . HostI)
  66         (.$)  = (<*>)
  67 instance Sym_Lambda TextI where
  68         lam f = TextI $ \po v ->
  69                 let x = "x" <> Text.pack (show v) in
  70                 infix_paren po op $
  71                         "\\" <> x <> " -> " <>
  72                         unTextI (f (TextI $ \_po _v -> x)) (op, L) (succ v)
  73                 where op = infixN 1
  74         -- (.$) = textI_infix "$" (Precedence 0)
  75         (.$) (TextI a1) (TextI a2) = TextI $ \po v ->
  76                 infix_paren po op $
  77                         a1 (op, L) v <> " " <> a2 (op, R) v
  78                 where op = infixN 10
  79         let_ e in_ =
  80                 TextI $ \po v ->
  81                         let x = "x" <> Text.pack (show v) in
  82                         infix_paren po op $
  83                         "let" <> " " <> x <> " = "
  84                          <> unTextI e (infixN 0, L) (succ v) <> " in "
  85                          <> unTextI (in_ (TextI $ \_po _v -> x)) (op, L) (succ v)
  86                 where op = infixN 2
  87         (^)   = textI_infix "." (infixR 9)
  88         id    = textI1 "id"
  89         const = textI2 "const"
  90         flip  = textI1 "flip"
  91 instance (Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (DupI r1 r2) where
  92         lam f = dupI_1 lam_f `DupI` dupI_2 lam_f
  93                 where lam_f = lam f
  94         (.$) = dupI2 (Proxy @Sym_Lambda) (.$)
  95
  96 instance
  97  ( Read_TypeNameR Type_Name cs rs
  98  , Inj_Const cs (->)
  99  ) => Read_TypeNameR Type_Name cs (Proxy (->) ': rs) where
 100         read_typenameR _cs (Type_Name "(->)") k = k (ty @(->))
 101         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
 102 instance Show_Const cs => Show_Const (Proxy (->) ': cs) where
 103         show_const ConstZ{} = "(->)"
 104         show_const (ConstS c) = show_const c
 105
 106 instance -- Proj_ConC (->)
 107  ( Proj_Const cs (->)
 108  , Proj_Consts cs (Consts_imported_by (->))
 109  , Proj_Con cs
 110  ) => Proj_ConC cs (Proxy (->)) where
 111         proj_conC _ (TyConst q :$ (TyConst c :$ _r))
 112          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 113          , Just Refl <- proj_const c (Proxy @(->))
 114          = case () of
 115                  _ | Just Refl <- proj_const q (Proxy @Functor)     -> Just Con
 116                    | Just Refl <- proj_const q (Proxy @Applicative) -> Just Con
 117                    | Just Refl <- proj_const q (Proxy @Monad)       -> Just Con
 118                  _ -> Nothing
 119         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ _a :$ b))
 120          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 121          , Just Refl <- proj_const c (Proxy @(->))
 122          = case () of
 123                  _ | Just Refl <- proj_const q (Proxy @Monoid)
 124                    , Just Con  <- proj_con (t :$ b) -> Just Con
 125                  _ -> Nothing
 126         proj_conC _c _q = Nothing
 127 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy (->)))
 128 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy (->)))
 129 instance -- CompileI (->)
 130  ( Inj_Const  (Consts_of_Ifaces is) (->)
 131  , Read_TypeName Type_Name (Consts_of_Ifaces is)
 132  , Compile is
 133  ) => CompileI is (Proxy (->)) where
 134         compileI tok ctx k =
 135                 case tok of
 136                  Token_Term_Abst name_arg tok_ty_arg tok_body ->
 137                         compile_type tok_ty_arg $ \(ty_arg::Type (Consts_of_Ifaces is) h) ->
 138                         check_kind
 139                          (At Nothing SKiType)
 140                          (At (Just $ tok_ty_arg) $ kind_of ty_arg) $ \Refl ->
 141                         compileO tok_body
 142                          (LamCtx_TypeS name_arg ty_arg ctx) $
 143                          \ty_res (TermO res) ->
 144                         k (ty_arg ~> ty_res) $ TermO $
 145                          \c -> lam $ \arg ->
 146                                 res (arg `LamCtx_TermS` c)
 147                  Token_Term_App tok_lam tok_arg_actual ->
 148                         compileO tok_lam ctx $ \ty_lam (TermO lam_) ->
 149                         compileO tok_arg_actual ctx $ \ty_arg_actual (TermO arg_actual) ->
 150                         check_type2 (ty @(->)) (At (Just tok_lam) ty_lam) $ \Refl ty_arg ty_res ->
 151                         check_type
 152                          (At (Just tok_lam) ty_arg)
 153                          (At (Just tok_arg_actual) ty_arg_actual) $ \Refl ->
 154                         k ty_res $ TermO $
 155                          \c -> lam_ c .$ arg_actual c
 156                  Token_Term_Let name tok_bound tok_body ->
 157                         compileO tok_bound ctx $ \ty_bound (TermO bound) ->
 158                         compileO tok_body (LamCtx_TypeS name ty_bound ctx) $
 159                          \ty_res (TermO res) ->
 160                         k ty_res $ TermO $
 161                          \c -> let_ (bound c) $ \arg -> res (arg `LamCtx_TermS` c)
 162                  Token_Term_Var nam -> go nam ctx k
 163                         where
 164                         go :: forall meta lc ret ls rs.
 165                             Term_Name
 166                          -> LamCtx_Type is Term_Name lc
 167                          -> ( forall h.
 168                                Type (Consts_of_Ifaces is) (h::Kind.Type)
 169                             -> TermO lc h is ls rs
 170                             -> Either (Error_Term meta is) ret )
 171                          -> Either (Error_Term meta is) ret
 172                         go name lc k' =
 173                                 case lc of
 174                                  LamCtx_TypeZ -> Left $ Error_Term_unbound name
 175                                  LamCtx_TypeS n typ _ | n == name ->
 176                                         k' typ $ TermO $ \(te `LamCtx_TermS` _) -> te
 177                                  LamCtx_TypeS _n _ty lc' ->
 178                                         go name lc' $ \typ (TermO te::TermO lc' h is '[] is) ->
 179                                         k' typ $ TermO $ \(_ `LamCtx_TermS` c) -> te c
 180                  Token_Term_Compose tok_f tok_g ->
 181                  -- (.) :: (b -> c) -> (a -> b) -> a -> c
 182                         compileO tok_f ctx $ \ty_f (TermO f) ->
 183                         compileO tok_g ctx $ \ty_g (TermO g) ->
 184                         check_type2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_b ty_c ->
 185                         check_type2 (ty @(->)) (At (Just tok_g) ty_g) $ \Refl ty_a ty_g_b ->
 186                         check_type
 187                          (At (Just tok_f) ty_f_b)
 188                          (At (Just tok_g) ty_g_b) $ \Refl ->
 189                         k (ty_a ~> ty_c) $ TermO $
 190                          \c -> (^) (f c) (g c)
 191 instance
 192  Inj_Token meta ts (->) =>
 193  TokenizeT meta ts (Proxy (->)) where
 194         tokenizeT _t = mempty
 195          { tokenizers_infix = tokenizeTMod []
 196                  [ tokenize2 "." (infixR 9) Token_Term_Compose
 197                  , tokenize2 "$" (infixR 0) Token_Term_App
 198                  ]
 199          }
 200 instance Gram_Term_AtomsT meta ts (Proxy (->)) g
 201
 202 -- | The function 'Type' @(->)@,
 203 -- with an infix notation more readable.
 204 (~>) :: forall cs a b. Inj_Const cs (->)
 205  => Type cs a -> Type cs b -> Type cs (a -> b)
 206 (~>) a b = ty @(->) :$ a :$ b
 207 infixr 5 ~>