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 ($$) = repr_dup2 sym_Lambda ($$)
85 sym_Lambda :: Proxy Sym_Lambda
88 -- * Type 'Expr_Lambda'
90 data Expr_Lambda (root:: *)
91 type instance Root_of_Expr (Expr_Lambda root) = root
92 type instance Type_of_Expr (Expr_Lambda root) = Type_Fun
93 type instance Sym_of_Expr (Expr_Lambda root) repr = Sym_Lambda repr
94 type instance Error_of_Expr ast (Expr_Lambda root) = Error_Expr_Lambda ast
96 -- | Parsing utility to check that the given type is a 'Type_Fun'
97 -- or raise 'Error_Expr_Type_mismatch'.
99 :: forall ast ex root ty h ret.
100 ( root ~ Root_of_Expr ex
101 , ty ~ Type_Root_of_Expr ex
102 , Type0_Lift Type_Fun (Type_of_Expr root)
103 , Type0_Unlift Type_Fun (Type_of_Expr root)
104 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
105 (Error_of_Expr ast root)
107 => Proxy ex -> ast -> ty h
108 -> (Type_Fun ty h -> Either (Error_of_Expr ast root) ret)
109 -> Either (Error_of_Expr ast root) ret
110 check_type_fun ex ast ty k =
111 case type0_unlift $ unType_Root ty of
115 Error_Expr_Type_mismatch ast
116 (Exists_Type0 (type_var0 SZero `type_fun` type_var0 (SSucc SZero)
117 :: ty ((->) Var0 Var0)))
120 -- | Parse a /lambda variable/.
122 :: forall ast root hs ret.
123 ( Type0_From ast (Type_Root_of_Expr root)
124 , Error_Expr_Lift (Error_Expr_Lambda ast)
125 (Error_of_Expr ast root)
126 , Root_of_Expr root ~ root
127 ) => Text -> ExprFrom ast (Expr_Lambda root) hs ret
128 var_from name _ex ast = go
130 go :: forall ex hs'. (ex ~ (Expr_Lambda root))
131 => Lambda_Context (Lambda_Var (Type_Root_of_Expr ex)) hs'
132 -> ( forall h. Type_Root_of_Expr ex h
133 -> Forall_Repr_with_Context ex hs' h
134 -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret )
135 -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret
138 Lambda_Context_Empty -> Left $ error_expr_lift $
139 Error_Expr_Lambda_Var_unbound name ast
140 Lambda_Var n ty `Lambda_Context_Next` _ | n == name ->
141 k' ty $ Forall_Repr_with_Context $
142 \(repr `Lambda_Context_Next` _) -> repr
143 _ `Lambda_Context_Next` ctx' ->
144 go ctx' $ \ty (Forall_Repr_with_Context repr) ->
145 k' ty $ Forall_Repr_with_Context $
146 \(_ `Lambda_Context_Next` c') -> repr c'
150 :: forall ty ast root hs ret.
151 ( ty ~ Type_Root_of_Expr root
155 , Type0_Lift Type_Fun (Type_of_Expr root)
156 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
157 (Error_of_Expr ast root)
158 , Type0_Unlift Type_Fun (Type_of_Expr root)
159 , Root_of_Expr root ~ root
161 -> ExprFrom ast (Expr_Lambda root) hs ret
162 app_from ast_lam ast_arg_actual ex ast ctx k =
163 expr_from (Proxy::Proxy root) ast_lam ctx $
164 \(ty_lam::ty h_lam) (Forall_Repr_with_Context l) ->
165 expr_from (Proxy::Proxy root) ast_arg_actual ctx $
166 \(ty_arg_actual::ty h_arg_actual)
167 (Forall_Repr_with_Context arg_actual) ->
168 case type0_unlift $ unType_Root ty_lam of
171 Error_Expr_Type_mismatch ast
172 (Exists_Type0 (type_var0 SZero `type_fun` type_var0 (SSucc SZero)
173 :: ty ((->) Var0 Var0)))
174 (Exists_Type0 ty_lam)
175 Just (Type2 Proxy ty_arg_expected ty_res
176 :: Type_Fun ty h_lam) ->
177 check_type0_eq ex ast
178 ty_arg_expected ty_arg_actual $ \Refl ->
179 k ty_res $ Forall_Repr_with_Context $
180 \c -> l c $$ arg_actual c
184 :: forall ty ast root hs ret.
185 ( ty ~ Type_Root_of_Expr root
186 , root ~ Root_of_Expr root
189 , Type0_Lift Type_Fun (Type_of_Expr root)
190 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
191 (Error_of_Expr ast root)
192 ) => Text -> ast -> ast
193 -> ExprFrom ast (Expr_Lambda root) hs ret
194 lam_from name ast_ty_arg ast_body ex ast ctx k =
195 case type0_from (Proxy::Proxy ty)
196 ast_ty_arg (Right . Exists_Type0) of
197 Left err -> Left $ error_expr ex $ Error_Expr_Type err ast
198 Right (Exists_Type0 (ty_arg::ty h_arg)) ->
199 expr_from (Proxy::Proxy root) ast_body
200 (Lambda_Var name ty_arg `Lambda_Context_Next` ctx) $
201 \(ty_res::ty h_res) (Forall_Repr_with_Context res) ->
202 k (ty_arg `type_fun` ty_res
203 :: Root_of_Type ty ((->) h_arg h_res)) $
204 Forall_Repr_with_Context $
206 \arg -> res (arg `Lambda_Context_Next` c)
210 :: forall ty ast root hs ret.
211 ( ty ~ Type_Root_of_Expr root
212 , root ~ Root_of_Expr root
215 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
216 (Error_of_Expr ast root)
217 ) => Text -> ast -> ast
218 -> ExprFrom ast (Expr_Lambda root) hs ret
219 let_from name ast_var ast_body _ex _ast ctx k =
220 expr_from (Proxy::Proxy root) ast_var ctx $
221 \(ty_var::ty h_var) (Forall_Repr_with_Context var) ->
222 expr_from (Proxy::Proxy root) ast_body
223 (Lambda_Var name ty_var `Lambda_Context_Next` ctx) $
224 \(ty_res::ty h_res) (Forall_Repr_with_Context res) ->
225 k ty_res $ Forall_Repr_with_Context $
227 \arg -> res (arg `Lambda_Context_Next` c)
229 -- * Type 'Error_Expr_Lambda'
230 data Error_Expr_Lambda ast
231 = Error_Expr_Lambda_Var_unbound Lambda_Var_Name ast