]> Git — Sourcephile - haskell/symantic.git/blob - Language/LOL/Symantic/Expr/Lambda.hs
init
[haskell/symantic.git] / Language / LOL / Symantic / Expr / Lambda.hs
1 {-# LANGUAGE DefaultSignatures #-}
2 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE FlexibleInstances #-}
4 {-# LANGUAGE GADTs #-}
5 {-# LANGUAGE MultiParamTypeClasses #-}
6 {-# LANGUAGE OverloadedStrings #-}
7 {-# LANGUAGE Rank2Types #-}
8 {-# LANGUAGE ScopedTypeVariables #-}
9 {-# LANGUAGE TypeFamilies #-}
10 {-# LANGUAGE UndecidableInstances #-}
11 -- | Expression for /lambda abstraction/s
12 -- in /Higher-Order Abstract Syntax/ (HOAS).
13 module Language.LOL.Symantic.Expr.Lambda where
14
15 import Data.Proxy (Proxy(..))
16 import Data.Type.Equality ((:~:)(Refl))
17
18 import Language.LOL.Symantic.AST
19 import Language.LOL.Symantic.Type
20 import Language.LOL.Symantic.Expr.Common
21 import Language.LOL.Symantic.Repr.Dup
22 import Language.LOL.Symantic.Trans.Common
23
24 -- * Class 'Sym_Lambda'
25
26 -- | Symantic.
27 --
28 -- NOTE: argument @arg@ and result @res@ of 'Lambda'
29 -- wrapped inside 'lam': to control the calling
30 -- in the 'Repr_Host' instance.
31 --
32 -- NOTE: the default definitions supplied for:
33 -- 'app', 'inline', 'val' and 'lazy'
34 -- are there to avoid boilerplate code
35 -- when writting 'Trans' instances which
36 -- do not need to alterate those methods.
37 class (lam ~ Lambda_from_Repr repr) => Sym_Lambda lam repr where
38 -- | This type constructor is used like
39 -- the functional dependency: @repr -> lam@
40 -- (ie. knowing @repr@ one can determine @lam@)
41 -- in order to avoid to introduce a 'Proxy' @lam@
42 -- in 'let_inline', 'let_val' and 'let_lazy'.
43 --
44 -- Distinguishing between @lam@ and @repr@ is used to maintain
45 -- the universal polymorphism of @repr@ in 'Expr_from',
46 -- the downside with this however is that
47 -- to be an instance of 'Sym_Lambda' for all @lam@,
48 -- the @repr@ type of an interpreter
49 -- has to be parameterized by @lam@,
50 -- even though it does not actually need @lam@ to do its work.
51 --
52 -- Basically this means having sometimes to add a type annotation
53 -- to the interpreter call to specify @lam@.
54 type Lambda_from_Repr repr :: {-lam-}(* -> *)
55
56 -- | Lambda application.
57 app :: repr (Lambda lam arg res) -> repr arg -> repr res
58
59 -- | /Call-by-name/ lambda.
60 inline :: (repr arg -> repr res) -> repr (Lambda lam arg res)
61 -- | /Call-by-value/ lambda.
62 val :: (repr arg -> repr res) -> repr (Lambda lam arg res)
63 -- | /Call-by-need/ lambda (aka. /lazyness/): lazy shares its argument, no matter what.
64 lazy :: (repr arg -> repr res) -> repr (Lambda lam arg res)
65
66 default app :: Trans t repr => t repr (Lambda lam arg res) -> t repr arg -> t repr res
67 default inline :: Trans t repr => (t repr arg -> t repr res) -> t repr (Lambda lam arg res)
68 default val :: Trans t repr => (t repr arg -> t repr res) -> t repr (Lambda lam arg res)
69 default lazy :: Trans t repr => (t repr arg -> t repr res) -> t repr (Lambda lam arg res)
70 app f x = trans_lift $ trans_apply f `app` trans_apply x
71 inline f = trans_lift $ inline $ trans_apply . f . trans_lift
72 val f = trans_lift $ val $ trans_apply . f . trans_lift
73 lazy f = trans_lift $ lazy $ trans_apply . f . trans_lift
74
75 -- | Convenient 'inline' wrapper.
76 let_inline
77 :: Sym_Lambda lam repr
78 => repr var -> (repr var -> repr res) -> repr res
79 let_inline x y = inline y `app` x
80 -- | Convenient 'val' wrapper.
81 let_val
82 :: Sym_Lambda lam repr
83 => repr var -> (repr var -> repr res) -> repr res
84 let_val x y = val y `app` x
85 -- | Convenient 'lazy' wrapper.
86 let_lazy
87 :: Sym_Lambda lam repr
88 => repr var -> (repr var -> repr res) -> repr res
89 let_lazy x y = lazy y `app` x
90
91 infixl 5 `app`
92
93 instance -- Sym_Lambda Dup
94 ( Sym_Lambda lam r1
95 , Sym_Lambda lam r2
96 ) => Sym_Lambda lam (Dup r1 r2) where
97 type Lambda_from_Repr (Dup r1 r2) = Lambda_from_Repr r1
98 app (f1 `Dup` f2) (x1 `Dup` x2) = app f1 x1 `Dup` app f2 x2
99 inline f = dup1 (inline f) `Dup` dup2 (inline f)
100 val f = dup1 (val f) `Dup` dup2 (val f)
101 lazy f = dup1 (lazy f) `Dup` dup2 (lazy f)
102
103 -- * Type 'Expr_Lambda'
104 -- | Expression.
105 data Expr_Lambda (lam:: * -> *) (root:: *)
106 type instance Root_of_Expr (Expr_Lambda lam root) = root
107 type instance Type_of_Expr (Expr_Lambda lam root) = Type_Fun lam
108 type instance Sym_of_Expr (Expr_Lambda lam root) repr = Sym_Lambda lam repr
109 type instance Error_of_Expr ast (Expr_Lambda lam root) = Error_Expr_Lambda ast
110
111 instance -- Expr_from AST Expr_Lambda
112 ( Type_from AST (Type_Root_of_Expr root)
113 , Expr_from AST root
114
115 , Type_Root_Lift (Type_Fun lam) (Type_Root_of_Expr root)
116 , Error_Expr_Lift (Error_Expr_Lambda AST)
117 (Error_of_Expr AST root)
118 , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
119 ( Type_Root_of_Expr root)
120 AST)
121 (Error_of_Expr AST root)
122 , Error_Expr_Unlift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
123 ( Type_Root_of_Expr root)
124 AST)
125 (Error_of_Expr AST root)
126
127 , Type_Unlift (Type_Fun lam) (Type_of_Expr root)
128
129 , Root_of_Expr root ~ root
130
131 , Implicit_HBool (Is_Last_Expr (Expr_Lambda lam root) root)
132 ) => Expr_from AST (Expr_Lambda lam root) where
133 expr_from px_ex ctx ast k =
134 case ast of
135 AST "var" asts ->
136 case asts of
137 [AST name []] -> go ctx k
138 where
139 go
140 :: forall hs ret
141 . Context (Lambda_Var (Type_Root_of_Expr root)) hs
142 -> ( forall h
143 . Type_Root_of_Expr root h
144 -> Forall_Repr_with_Context (Expr_Lambda lam root) hs h
145 -> Either (Error_of_Expr AST root) ret )
146 -> Either (Error_of_Expr AST root) ret
147 go c k' =
148 case c of
149 Context_Empty -> Left $ error_expr_lift $
150 Error_Expr_Lambda_Var_unbound name ast
151 Lambda_Var n ty `Context_Next` _ | n == name ->
152 k' ty $ Forall_Repr_with_Context $
153 \(repr `Context_Next` _) -> repr
154 _ `Context_Next` ctx' ->
155 go ctx' $ \ty (Forall_Repr_with_Context repr) ->
156 k' ty $ Forall_Repr_with_Context $
157 \(_ `Context_Next` c') -> repr c'
158 _ -> Left $ error_expr px_ex $
159 Error_Expr_Wrong_number_of_arguments ast 1
160 AST "app" asts ->
161 case asts of
162 [ast_lam, ast_arg_actual] ->
163 expr_from (Proxy::Proxy root) ctx ast_lam $
164 \(ty_lam::Type_Root_of_Expr root h_lam) (Forall_Repr_with_Context lam) ->
165 expr_from (Proxy::Proxy root) ctx ast_arg_actual $
166 \(ty_arg_actual::Type_Root_of_Expr root h_arg_actual)
167 (Forall_Repr_with_Context arg_actual) ->
168 case type_unlift $ unType_Root ty_lam of
169 Nothing -> Left $
170 error_expr px_ex $
171 Error_Expr_Type_mismatch ast
172 (Exists_Type (type_var SZero `type_fun` type_var (SSucc SZero)
173 :: Type_Root_of_Expr (Expr_Lambda lam root) (lam Zero -> lam (Succ Zero))))
174 (Exists_Type ty_lam)
175 Just (ty_arg_expected `Type_Fun` ty_res
176 :: Type_Fun lam (Type_Root_of_Expr root) h_lam) ->
177 when_type_eq px_ex ast
178 ty_arg_expected ty_arg_actual $ \Refl ->
179 k ty_res $ Forall_Repr_with_Context $
180 \c -> lam c `app` arg_actual c
181 _ -> Left $ error_expr px_ex $
182 Error_Expr_Type (error_type_lift $
183 Error_Type_Wrong_number_of_arguments ast 2) ast
184 AST "inline" asts -> lambda_from asts inline
185 AST "val" asts -> lambda_from asts val
186 AST "lazy" asts -> lambda_from asts lazy
187 AST "let_inline" asts -> let_from asts let_inline
188 AST "let_val" asts -> let_from asts let_val
189 AST "let_lazy" asts -> let_from asts let_lazy
190 _ -> Left $ error_expr_unsupported px_ex ast
191 where
192 lambda_from asts
193 (lam::forall repr arg res. Sym_Lambda lam repr
194 => (repr arg -> repr res) -> repr (Lambda lam arg res)) =
195 case asts of
196 [AST name [], ast_ty_arg, ast_body] ->
197 case type_from
198 (Proxy::Proxy (Type_Root_of_Expr root))
199 ast_ty_arg (Right . Exists_Type) of
200 Left err -> Left $ error_expr px_ex $ Error_Expr_Type err ast
201 Right (Exists_Type (ty_arg::Type_Root_of_Expr root h_arg)) ->
202 expr_from (Proxy::Proxy root)
203 (Lambda_Var name ty_arg `Context_Next` ctx) ast_body $
204 \(ty_res::Type_Root_of_Expr root h_res) (Forall_Repr_with_Context res) ->
205 k (ty_arg `type_fun` ty_res
206 :: Root_of_Type (Type_Root_of_Expr root)
207 (Lambda lam h_arg h_res)) $
208 Forall_Repr_with_Context $
209 \c -> lam $
210 \arg -> res (arg `Context_Next` c)
211 _ -> Left $ error_expr px_ex $
212 Error_Expr_Wrong_number_of_arguments ast 3
213 let_from asts
214 (let_::forall repr var res. Sym_Lambda lam repr
215 => repr var -> (repr var -> repr res) -> repr res) =
216 case asts of
217 [AST name [], ast_var, ast_body] ->
218 expr_from (Proxy::Proxy root) ctx ast_var $
219 \(ty_var::Type_Root_of_Expr root h_var) (Forall_Repr_with_Context var) ->
220 expr_from (Proxy::Proxy root)
221 (Lambda_Var name ty_var `Context_Next` ctx) ast_body $
222 \(ty_res::Type_Root_of_Expr root h_res) (Forall_Repr_with_Context res) ->
223 k ty_res $ Forall_Repr_with_Context $
224 \c -> let_ (var c) $
225 \arg -> res (arg `Context_Next` c)
226 _ -> Left $ error_expr px_ex $
227 Error_Expr_Wrong_number_of_arguments ast 3
228
229 -- * Type 'Error_Expr_Lambda'
230 data Error_Expr_Lambda ast
231 = Error_Expr_Lambda_Var_unbound Var_Name ast
232 deriving (Eq, Show)