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         (#) :: repr (b -> c) -> repr (a -> b) -> repr a -> repr c
  57         (#) f g a = f $$ (g $$ a)
  58
  59         flip :: repr (a -> b -> c) -> repr b -> repr a -> repr c
  60         flip f b a = f $$ a $$ b
  61 infixl 0 $$
  62 infixr 9 #
  63 instance Sym_Lambda Repr_Host where
  64         ($$)  = (Applicative.<*>)
  65         lam f = Repr_Host (unRepr_Host . f . Repr_Host)
  66 instance Sym_Lambda Repr_Text where
  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         lam f =
  72                 Repr_Text $ \p v ->
  73                         let p' = precedence_Lambda in
  74                         let x = "x" <> Text.pack (show v) in
  75                         paren p p' $
  76                         "\\" <> x <> " -> " <>
  77                         unRepr_Text (f (Repr_Text $ \_p _v -> x)) p' (succ v)
  78         let_ e in_ =
  79                 Repr_Text $ \p v ->
  80                         let p' = precedence_Let in
  81                         let x = "x" <> Text.pack (show v) in
  82                         paren p p' $
  83                         "let" <> " " <> x <> " = " <> unRepr_Text e p (succ v) <> " in " <>
  84                         unRepr_Text (in_ (Repr_Text $ \_p _v -> x)) p (succ v)
  85 instance
  86  ( Sym_Lambda r1
  87  , Sym_Lambda r2
  88  ) => Sym_Lambda (Dup r1 r2) where
  89         ($$) (f1 `Dup` f2) (x1 `Dup` x2) = ($$) f1 x1 `Dup` ($$) f2 x2
  90         lam f = dup1 (lam f) `Dup` dup2 (lam f)
  91
  92 -- * Type 'Expr_Lambda'
  93 -- | Expression.
  94 data Expr_Lambda (root:: *)
  95 type instance Root_of_Expr      (Expr_Lambda root)      = root
  96 type instance Type_of_Expr      (Expr_Lambda root)      = Type_Fun
  97 type instance Sym_of_Expr       (Expr_Lambda root) repr = Sym_Lambda repr
  98 type instance Error_of_Expr ast (Expr_Lambda root)      = Error_Expr_Lambda ast
  99
 100 -- | Parsing utility to check that the given type is a 'Type_Fun'
 101 -- or raise 'Error_Expr_Type_mismatch'.
 102 check_type_fun
 103  :: forall ast ex root ty h ret.
 104  ( root ~ Root_of_Expr ex
 105  , ty ~ Type_Root_of_Expr ex
 106  , Lift_Type   Type_Fun (Type_of_Expr root)
 107  , Unlift_Type Type_Fun (Type_of_Expr root)
 108  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 109                    (Error_of_Expr ast root)
 110  )
 111  => Proxy ex -> ast -> ty h
 112  -> (Type_Fun ty h -> Either (Error_of_Expr ast root) ret)
 113  -> Either (Error_of_Expr ast root) ret
 114 check_type_fun ex ast ty k =
 115         case unlift_type $ unType_Root ty of
 116          Just ty_f -> k ty_f
 117          Nothing -> Left $
 118                 error_expr ex $
 119                 Error_Expr_Type_mismatch ast
 120                  (Exists_Type (type_var0 SZero `type_fun` type_var0 (SSucc SZero)
 121                  :: ty ((->) Var0 Var0)))
 122                  (Exists_Type ty)
 123
 124 -- | Parse a /lambda variable/.
 125 var_from
 126  :: forall ast root hs ret.
 127  ( Type_from ast (Type_Root_of_Expr root)
 128  , Lift_Error_Expr (Error_Expr_Lambda ast)
 129                    (Error_of_Expr ast root)
 130  , Root_of_Expr root ~ root
 131  ) => Text -> Expr_From ast (Expr_Lambda root) hs ret
 132 var_from name _ex ast = go
 133         where
 134         go :: forall ex hs'. (ex ~ (Expr_Lambda root))
 135          => Context (Lambda_Var (Type_Root_of_Expr ex)) hs'
 136          -> ( forall h. Type_Root_of_Expr ex h
 137             -> Forall_Repr_with_Context ex hs' h
 138             -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret )
 139          ->    Either (Error_of_Expr ast (Root_of_Expr ex)) ret
 140         go c k' =
 141                 case c of
 142                  Context_Empty -> Left $ lift_error_expr $
 143                         Error_Expr_Lambda_Var_unbound name ast
 144                  Lambda_Var n ty `Context_Next` _ | n == name ->
 145                         k' ty $ Forall_Repr_with_Context $
 146                          \(repr `Context_Next` _) -> repr
 147                  _ `Context_Next` ctx' ->
 148                         go ctx' $ \ty (Forall_Repr_with_Context repr) ->
 149                                 k' ty $ Forall_Repr_with_Context $
 150                                  \(_ `Context_Next` c') -> repr c'
 151
 152 -- | Parse 'app'.
 153 app_from
 154  :: forall ty ast root hs ret.
 155  ( ty ~ Type_Root_of_Expr root
 156  , Type_from ast ty
 157  , Eq_Type ty
 158  , Expr_from ast root
 159  , Lift_Type Type_Fun (Type_of_Expr root)
 160  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 161                    (Error_of_Expr ast root)
 162  , Unlift_Type Type_Fun (Type_of_Expr root)
 163  , Root_of_Expr root ~ root
 164  ) => ast -> ast
 165  -> Expr_From ast (Expr_Lambda root) hs ret
 166 app_from ast_lam ast_arg_actual ex ast ctx k =
 167         expr_from (Proxy::Proxy root) ast_lam ctx $
 168          \(ty_lam::ty h_lam) (Forall_Repr_with_Context l) ->
 169         expr_from (Proxy::Proxy root) ast_arg_actual ctx $
 170          \(ty_arg_actual::ty h_arg_actual)
 171           (Forall_Repr_with_Context arg_actual) ->
 172                 case unlift_type $ unType_Root ty_lam of
 173                  Nothing -> Left $
 174                         error_expr ex $
 175                         Error_Expr_Type_mismatch ast
 176                          (Exists_Type (type_var0 SZero `type_fun` type_var0 (SSucc SZero)
 177                          :: ty ((->) Var0 Var0)))
 178                          (Exists_Type ty_lam)
 179                  Just (Type_Type2 Proxy ty_arg_expected ty_res
 180                   :: Type_Fun ty h_lam) ->
 181                         check_eq_type ex ast
 182                          ty_arg_expected ty_arg_actual $ \Refl ->
 183                                 k ty_res $ Forall_Repr_with_Context $
 184                                  \c -> l c $$ arg_actual c
 185
 186 -- | Parse given /lambda abstraction/.
 187 lam_from
 188  :: forall ty ast root hs ret.
 189  ( ty ~ Type_Root_of_Expr root
 190  , root ~ Root_of_Expr root
 191  , Type_from ast ty
 192  , Expr_from ast root
 193  , Lift_Type Type_Fun (Type_of_Expr root)
 194  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 195                    (Error_of_Expr ast root)
 196  ) => Text -> ast -> ast
 197  -> Expr_From ast (Expr_Lambda root) hs ret
 198 lam_from name ast_ty_arg ast_body ex ast ctx k =
 199         case type_from
 200          (Proxy::Proxy ty)
 201          ast_ty_arg (Right . Exists_Type) of
 202          Left err -> Left $ error_expr ex $ Error_Expr_Type err ast
 203          Right (Exists_Type (ty_arg::ty h_arg)) ->
 204                 expr_from (Proxy::Proxy root) ast_body
 205                  (Lambda_Var name ty_arg `Context_Next` ctx) $
 206                  \(ty_res::ty h_res) (Forall_Repr_with_Context res) ->
 207                         k (ty_arg `type_fun` ty_res
 208                          :: Root_of_Type ty ((->) h_arg h_res)) $
 209                         Forall_Repr_with_Context $
 210                          \c -> lam $
 211                                  \arg -> res (arg `Context_Next` c)
 212
 213 -- | Parse given /let/.
 214 let_from
 215  :: forall ty ast root hs ret.
 216  ( ty ~ Type_Root_of_Expr root
 217  , root ~ Root_of_Expr root
 218  , Type_from ast ty
 219  , Expr_from ast root
 220  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 221                    (Error_of_Expr ast root)
 222  ) => Text -> ast -> ast
 223  -> Expr_From ast (Expr_Lambda root) hs ret
 224 let_from name ast_var ast_body _ex _ast ctx k =
 225         expr_from (Proxy::Proxy root) ast_var ctx $
 226          \(ty_var::ty h_var) (Forall_Repr_with_Context var) ->
 227                 expr_from (Proxy::Proxy root) ast_body
 228                  (Lambda_Var name ty_var `Context_Next` ctx) $
 229                  \(ty_res::ty h_res) (Forall_Repr_with_Context res) ->
 230                         k ty_res $ Forall_Repr_with_Context $
 231                          \c -> let_ (var c) $
 232                                  \arg -> res (arg `Context_Next` c)
 233
 234 -- * Type 'Error_Expr_Lambda'
 235 data Error_Expr_Lambda ast
 236  =   Error_Expr_Lambda_Var_unbound Lambda_Var_Name ast
 237  deriving (Eq, Show)