Language/Symantic/Expr/Lambda.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE DataKinds #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE OverloadedStrings #-}
   7 {-# LANGUAGE Rank2Types #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE TypeFamilies #-}
  10 {-# LANGUAGE TypeOperators #-}
  11 -- | Expression for /lambda abstraction/s
  12 -- in /Higher-Order Abstract Syntax/ (HOAS).
  13 module Language.Symantic.Expr.Lambda where
  14
  15 import qualified Control.Applicative as Applicative
  16 import qualified Data.Function as Fun
  17 import Data.Monoid
  18 import Data.Proxy (Proxy(..))
  19 import Data.Type.Equality ((:~:)(Refl))
  20 import Data.Text (Text)
  21 import qualified Data.Text as Text
  22 import Prelude hiding (const, id)
  23
  24 import Language.Symantic.Type
  25 import Language.Symantic.Repr
  26 import Language.Symantic.Expr.Root
  27 import Language.Symantic.Expr.Error
  28 import Language.Symantic.Expr.From
  29 import Language.Symantic.Trans.Common
  30
  31 -- * Class 'Sym_Lambda'
  32 -- | Symantic.
  33 class Sym_Lambda repr where
  34         -- | /Lambda application/.
  35         ($$) :: repr ((->) arg res) -> repr arg -> repr res
  36         default ($$) :: Trans t repr
  37          => t repr ((->) arg res) -> t repr arg -> t repr res
  38         ($$) f x = trans_lift (trans_apply f $$ trans_apply x)
  39
  40         -- | /Lambda abstraction/.
  41         lam :: (repr arg -> repr res) -> repr ((->) arg res)
  42         default lam :: Trans t repr
  43          => (t repr arg -> t repr res) -> t repr ((->) arg res)
  44         lam f = trans_lift $ lam $ trans_apply . f . trans_lift
  45
  46         -- | Convenient 'lam' and '$$' wrapper.
  47         let_ :: repr var -> (repr var -> repr res) -> repr res
  48         let_ x y = lam y $$ x
  49
  50         id :: repr a -> repr a
  51         id a = (lam Fun.id) $$ a
  52
  53         const :: repr a -> repr b -> repr a
  54         const a b = lam (lam . Fun.const) $$ a $$ b
  55
  56         -- | /Lambda composition/.
  57         (#) :: repr (b -> c) -> repr (a -> b) -> repr (a -> c)
  58         (#) f g = lam $ \a -> f $$ (g $$ a)
  59
  60         flip :: repr (a -> b -> c) -> repr (b -> a -> c)
  61         flip f = lam $ \b -> lam $ \a -> f $$ a $$ b
  62
  63 infixl 0 $$
  64 infixr 9 #
  65
  66 instance Sym_Lambda Repr_Host where
  67         ($$)  = (Applicative.<*>)
  68         lam f = Repr_Host (unRepr_Host . f . Repr_Host)
  69 instance Sym_Lambda Repr_Text where
  70         -- ($$) = repr_text_infix "$" (Precedence 0)
  71         ($$) (Repr_Text a1) (Repr_Text a2) =
  72                 Repr_Text $ \p v ->
  73                         let p' = precedence_App in
  74                         paren p p' $ a1 p' v <> " " <> a2 p' v
  75         lam f =
  76                 Repr_Text $ \p v ->
  77                         let p' = Precedence 1 in
  78                         let x = "x" <> Text.pack (show v) in
  79                         paren p p' $ "\\" <> x <> " -> "
  80                          <> unRepr_Text (f (Repr_Text $ \_p _v -> x)) p' (succ v)
  81         let_ e in_ =
  82                 Repr_Text $ \p v ->
  83                         let p' = Precedence 2 in
  84                         let x = "x" <> Text.pack (show v) in
  85                         paren p p' $ "let" <> " " <> x <> " = "
  86                          <> unRepr_Text e (Precedence 0) (succ v) <> " in "
  87                          <> unRepr_Text (in_ (Repr_Text $ \_p _v -> x)) p' (succ v)
  88         (#)   = repr_text_infix "." (Precedence 9)
  89         id    = repr_text_app1 "id"
  90         const = repr_text_app2 "const"
  91         flip  = repr_text_app1 "flip"
  92 instance (Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (Repr_Dup r1 r2) where
  93         ($$) (f1 `Repr_Dup` f2) (x1 `Repr_Dup` x2) = ($$) f1 x1 `Repr_Dup` ($$) f2 x2
  94         lam f = repr_dup_1 (lam f) `Repr_Dup` repr_dup_2 (lam f)
  95
  96 -- * Type 'Expr_Lambda'
  97 -- | Expression.
  98 data Expr_Lambda (root:: *)
  99 type instance Root_of_Expr      (Expr_Lambda root)      = root
 100 type instance Type_of_Expr      (Expr_Lambda root)      = Type_Fun
 101 type instance Sym_of_Expr       (Expr_Lambda root) repr = Sym_Lambda repr
 102 type instance Error_of_Expr ast (Expr_Lambda root)      = Error_Expr_Lambda ast
 103
 104 -- | Parsing utility to check that the given type is a 'Type_Fun'
 105 -- or raise 'Error_Expr_Type_mismatch'.
 106 check_type_fun
 107  :: forall ast ex root ty h ret.
 108  ( root ~ Root_of_Expr ex
 109  , ty ~ Type_Root_of_Expr ex
 110  , Type0_Lift   Type_Fun (Type_of_Expr root)
 111  , Type0_Unlift Type_Fun (Type_of_Expr root)
 112  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 113                    (Error_of_Expr ast root)
 114  )
 115  => Proxy ex -> ast -> ty h
 116  -> (Type_Fun ty h -> Either (Error_of_Expr ast root) ret)
 117  -> Either (Error_of_Expr ast root) ret
 118 check_type_fun ex ast ty k =
 119         case type0_unlift $ unType_Root ty of
 120          Just ty_f -> k ty_f
 121          Nothing -> Left $
 122                 error_expr ex $
 123                 Error_Expr_Type_mismatch ast
 124                  (Exists_Type0 (type_var0 SZero `type_fun` type_var0 (SSucc SZero)
 125                  :: ty ((->) Var0 Var0)))
 126                  (Exists_Type0 ty)
 127
 128 -- | Parse a /lambda variable/.
 129 var_from
 130  :: forall ast root hs ret.
 131  ( Type0_From ast (Type_Root_of_Expr root)
 132  , Error_Expr_Lift (Error_Expr_Lambda ast)
 133                    (Error_of_Expr ast root)
 134  , Root_of_Expr root ~ root
 135  ) => Text -> ExprFrom ast (Expr_Lambda root) hs ret
 136 var_from name _ex ast = go
 137         where
 138         go :: forall ex hs'. (ex ~ (Expr_Lambda root))
 139          => Lambda_Context (Lambda_Var (Type_Root_of_Expr ex)) hs'
 140          -> ( forall h. Type_Root_of_Expr ex h
 141             -> Forall_Repr_with_Context ex hs' h
 142             -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret )
 143          ->    Either (Error_of_Expr ast (Root_of_Expr ex)) ret
 144         go c k' =
 145                 case c of
 146                  Lambda_Context_Empty -> Left $ error_expr_lift $
 147                         Error_Expr_Lambda_Var_unbound name ast
 148                  Lambda_Var n ty `Lambda_Context_Next` _ | n == name ->
 149                         k' ty $ Forall_Repr_with_Context $
 150                          \(repr `Lambda_Context_Next` _) -> repr
 151                  _ `Lambda_Context_Next` ctx' ->
 152                         go ctx' $ \ty (Forall_Repr_with_Context repr) ->
 153                                 k' ty $ Forall_Repr_with_Context $
 154                                  \(_ `Lambda_Context_Next` c') -> repr c'
 155
 156 -- | Parse '$$'.
 157 app_from
 158  :: forall ty ast root hs ret.
 159  ( ty ~ Type_Root_of_Expr root
 160  , Type0_From ast ty
 161  , Type0_Eq ty
 162  , Expr_From ast root
 163  , Type0_Lift Type_Fun (Type_of_Expr root)
 164  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 165                    (Error_of_Expr ast root)
 166  , Type0_Unlift Type_Fun (Type_of_Expr root)
 167  , Root_of_Expr root ~ root
 168  ) => ast -> ast
 169  -> ExprFrom ast (Expr_Lambda root) hs ret
 170 app_from ast_lam ast_arg_actual ex ast ctx k =
 171         expr_from (Proxy::Proxy root) ast_lam ctx $
 172          \(ty_lam::ty h_lam) (Forall_Repr_with_Context l) ->
 173         expr_from (Proxy::Proxy root) ast_arg_actual ctx $
 174          \(ty_arg_actual::ty h_arg_actual)
 175           (Forall_Repr_with_Context arg_actual) ->
 176                 case type0_unlift $ unType_Root ty_lam of
 177                  Nothing -> Left $
 178                         error_expr ex $
 179                         Error_Expr_Type_mismatch ast
 180                          (Exists_Type0 (type_var0 SZero `type_fun` type_var0 (SSucc SZero)
 181                          :: ty ((->) Var0 Var0)))
 182                          (Exists_Type0 ty_lam)
 183                  Just (Type2 Proxy ty_arg_expected ty_res
 184                   :: Type_Fun ty h_lam) ->
 185                         check_type0_eq ex ast
 186                          ty_arg_expected ty_arg_actual $ \Refl ->
 187                                 k ty_res $ Forall_Repr_with_Context $
 188                                  \c -> l c $$ arg_actual c
 189
 190 -- | Parse 'lam'.
 191 lam_from
 192  :: forall ty ast root hs ret.
 193  ( ty ~ Type_Root_of_Expr root
 194  , root ~ Root_of_Expr root
 195  , Type0_From ast ty
 196  , Expr_From ast root
 197  , Type0_Lift Type_Fun (Type_of_Expr root)
 198  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 199                    (Error_of_Expr ast root)
 200  ) => Text -> ast -> ast
 201  -> ExprFrom ast (Expr_Lambda root) hs ret
 202 lam_from name ast_ty_arg ast_body ex ast ctx k =
 203         case type0_from (Proxy::Proxy ty)
 204          ast_ty_arg (Right . Exists_Type0) of
 205          Left err -> Left $ error_expr ex $ Error_Expr_Type err ast
 206          Right (Exists_Type0 (ty_arg::ty h_arg)) ->
 207                 expr_from (Proxy::Proxy root) ast_body
 208                  (Lambda_Var name ty_arg `Lambda_Context_Next` ctx) $
 209                  \(ty_res::ty h_res) (Forall_Repr_with_Context res) ->
 210                         k (ty_arg `type_fun` ty_res
 211                          :: Root_of_Type ty ((->) h_arg h_res)) $
 212                         Forall_Repr_with_Context $
 213                          \c -> lam $
 214                                  \arg -> res (arg `Lambda_Context_Next` c)
 215
 216 -- | Parse 'let_'.
 217 let_from
 218  :: forall ty ast root hs ret.
 219  ( ty ~ Type_Root_of_Expr root
 220  , root ~ Root_of_Expr root
 221  , Type0_From ast ty
 222  , Expr_From ast root
 223  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 224                    (Error_of_Expr ast root)
 225  ) => Text -> ast -> ast
 226  -> ExprFrom ast (Expr_Lambda root) hs ret
 227 let_from name ast_var ast_body _ex _ast ctx k =
 228         expr_from (Proxy::Proxy root) ast_var ctx $
 229          \(ty_var::ty h_var) (Forall_Repr_with_Context var) ->
 230                 expr_from (Proxy::Proxy root) ast_body
 231                  (Lambda_Var name ty_var `Lambda_Context_Next` ctx) $
 232                  \(ty_res::ty h_res) (Forall_Repr_with_Context res) ->
 233                         k ty_res $ Forall_Repr_with_Context $
 234                          \c -> let_ (var c) $
 235                                  \arg -> res (arg `Lambda_Context_Next` c)
 236
 237 -- * Type 'Error_Expr_Lambda'
 238 data Error_Expr_Lambda ast
 239  =   Error_Expr_Lambda_Var_unbound Lambda_Var_Name ast
 240  deriving (Eq, Show)