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