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
18 import qualified Control.Applicative as Applicative
19 import qualified Data.Function as Fun
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)
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
34 -- * Class 'Sym_Lambda'
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)
43 -- | Convenient 'lam' and '$$' wrapper.
44 let_ :: repr var -> (repr var -> repr res) -> repr res
47 id :: repr a -> repr a
48 id a = (lam Fun.id) $$ a
50 const :: repr a -> repr b -> repr a
51 const a b = lam (lam . Fun.const) $$ a $$ b
53 -- | /Lambda composition/.
54 (#) :: repr (b -> c) -> repr (a -> b) -> repr (a -> c)
55 (#) f g = lam $ \a -> f $$ (g $$ a)
57 flip :: repr (a -> b -> c) -> repr (b -> a -> c)
58 flip f = lam $ \b -> lam $ \a -> f $$ a $$ b
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) =
69 let p' = precedence_App in
70 paren p p' $ a1 p' v <> " " <> a2 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
85 -- * Type 'Expr_Lambda'
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
93 -- | Parsing utility to check that the given type is a 'Type_Fun'
94 -- or raise 'Error_Expr_Type_mismatch'.
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)
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
112 Error_Expr_Type_mismatch ast
113 (Exists_Type0 (type_var0 SZero `type_fun` type_var0 (SSucc SZero)
114 :: ty ((->) Var0 Var0)))
117 -- | Parse a /lambda variable/.
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
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
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'
147 :: forall ty ast root hs ret.
148 ( ty ~ Type_Root_of_Expr 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
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
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
181 :: forall ty ast root hs ret.
182 ( ty ~ Type_Root_of_Expr root
183 , root ~ Root_of_Expr 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 $
203 \arg -> res (arg `Lambda_Context_Next` c)
207 :: forall ty ast root hs ret.
208 ( ty ~ Type_Root_of_Expr root
209 , root ~ Root_of_Expr 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 $
224 \arg -> res (arg `Lambda_Context_Next` c)
226 -- * Type 'Error_Expr_Lambda'
227 data Error_Expr_Lambda ast
228 = Error_Expr_Lambda_Var_unbound Lambda_Var_Name ast