]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Lambda.hs
Fix comment typo.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Lambda.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE GADTs #-}
3 {-# LANGUAGE PolyKinds #-}
4 {-# LANGUAGE UndecidableInstances #-}
5 {-# OPTIONS_GHC -fno-warn-orphans #-}
6 -- | Symantic for '(->)'.
7 module Language.Symantic.Lib.Lambda where
8
9 import qualified Data.Function as Fun
10 import qualified Data.Kind as Kind
11 import Data.Monoid ((<>))
12 import Data.Proxy (Proxy(..))
13 import qualified Data.Text as Text
14 import Data.Type.Equality ((:~:)(..))
15 import Prelude hiding ((^))
16
17 import Language.Symantic.Parsing
18 import Language.Symantic.Typing
19 import Language.Symantic.Compiling
20 import Language.Symantic.Interpreting
21 import Language.Symantic.Transforming
22
23
24 -- * Class 'Sym_Lambda'
25 class Sym_Lambda term where
26 -- | /Lambda abstraction/.
27 lam :: (term arg -> term res) -> term (arg -> res)
28 default lam :: Trans t term => (t term arg -> t term res) -> t term (arg -> res)
29 lam f = trans_lift $ lam $ trans_apply . f . trans_lift
30
31 -- | /Lambda application/.
32 (.$) :: term (arg -> res) -> term arg -> term res
33 default (.$) :: Trans t term => t term (arg -> res) -> t term arg -> t term res
34 infixr 0 .$
35 (.$) f x = trans_lift (trans_apply f .$ trans_apply x)
36
37 -- | Convenient 'lam' and '.$' wrapper.
38 let_ :: term var -> (term var -> term res) -> term res
39 let_ x y = lam y .$ x
40
41 id :: term a -> term a
42 id a = lam Fun.id .$ a
43
44 const :: term a -> term b -> term a
45 const a b = (lam (lam . Fun.const) .$ a) .$ b
46
47 -- | /Lambda composition/.
48 (^) :: term (b -> c) -> term (a -> b) -> term (a -> c)
49 (^) f g = lam $ \a -> f .$ (g .$ a)
50 infixr 9 ^
51
52 flip :: term (a -> b -> c) -> term (b -> a -> c)
53 flip f = lam $ \b -> lam $ \a -> (f .$ a) .$ b
54
55 type instance Sym_of_Iface (Proxy (->)) = Sym_Lambda
56 type instance TyConsts_of_Iface (Proxy (->)) = Proxy (->) ': TyConsts_imported_by (->)
57 type instance TyConsts_imported_by (->) =
58 [ Proxy Applicative
59 , Proxy Functor
60 , Proxy Monad
61 , Proxy Monoid
62 ]
63
64 instance Sym_Lambda HostI where
65 lam f = HostI (unHostI . f . HostI)
66 (.$) = (<*>)
67 instance Sym_Lambda TextI where
68 lam f = TextI $ \po v ->
69 let x = "x" <> Text.pack (show v) in
70 infix_paren po op $
71 "\\" <> x <> " -> " <>
72 unTextI (f (TextI $ \_po _v -> x)) (op, L) (succ v)
73 where op = infixN 1
74 -- (.$) = textI_infix "$" (Precedence 0)
75 (.$) (TextI a1) (TextI a2) = TextI $ \po v ->
76 infix_paren po op $
77 a1 (op, L) v <> " " <> a2 (op, R) v
78 where op = infixN 10
79 let_ e in_ =
80 TextI $ \po v ->
81 let x = "x" <> Text.pack (show v) in
82 infix_paren po op $
83 "let" <> " " <> x <> " = "
84 <> unTextI e (infixN 0, L) (succ v) <> " in "
85 <> unTextI (in_ (TextI $ \_po _v -> x)) (op, L) (succ v)
86 where op = infixN 2
87 (^) = textI_infix "." (infixR 9)
88 id = textI1 "id"
89 const = textI2 "const"
90 flip = textI1 "flip"
91 instance (Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (DupI r1 r2) where
92 lam f = dupI_1 lam_f `DupI` dupI_2 lam_f
93 where lam_f = lam f
94 (.$) = dupI2 @Sym_Lambda (.$)
95
96 instance
97 ( Read_TyNameR TyName cs rs
98 , Inj_TyConst cs (->)
99 ) => Read_TyNameR TyName cs (Proxy (->) ': rs) where
100 read_TyNameR _cs (TyName "(->)") k = k (ty @(->))
101 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
102 instance Show_TyConst cs => Show_TyConst (Proxy (->) ': cs) where
103 show_TyConst TyConstZ{} = "(->)"
104 show_TyConst (TyConstS c) = show_TyConst c
105
106 instance -- Proj_TyConC (->)
107 ( Proj_TyConst cs (->)
108 , Proj_TyConsts cs (TyConsts_imported_by (->))
109 , Proj_TyCon cs
110 ) => Proj_TyConC cs (Proxy (->)) where
111 proj_TyConC _ (TyConst q :$ (TyConst c :$ _r))
112 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
113 , Just Refl <- proj_TyConst c (Proxy @(->))
114 = case () of
115 _ | Just Refl <- proj_TyConst q (Proxy @Functor) -> Just TyCon
116 | Just Refl <- proj_TyConst q (Proxy @Applicative) -> Just TyCon
117 | Just Refl <- proj_TyConst q (Proxy @Monad) -> Just TyCon
118 _ -> Nothing
119 proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ _a :$ b))
120 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
121 , Just Refl <- proj_TyConst c (Proxy @(->))
122 = case () of
123 _ | Just Refl <- proj_TyConst q (Proxy @Monoid)
124 , Just TyCon <- proj_TyCon (t :$ b) -> Just TyCon
125 _ -> Nothing
126 proj_TyConC _c _q = Nothing
127 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy (->)))
128 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy (->)))
129 instance -- CompileI (->)
130 ( Inj_TyConst (TyConsts_of_Ifaces is) (->)
131 , Read_TyName TyName (TyConsts_of_Ifaces is)
132 , Compile is
133 ) => CompileI is (Proxy (->)) where
134 compileI tok ctx k =
135 case tok of
136 Token_Term_Abst name_arg tok_ty_arg tok_body ->
137 compile_Type tok_ty_arg $ \(ty_arg::Type (TyConsts_of_Ifaces is) h) ->
138 check_Kind
139 (At Nothing SKiType)
140 (At (Just $ tok_ty_arg) $ kind_of ty_arg) $ \Refl ->
141 compileO tok_body
142 (LamCtx_TypeS name_arg ty_arg ctx) $
143 \ty_res (TermO res) ->
144 k (ty_arg ~> ty_res) $ TermO $
145 \c -> lam $ \arg ->
146 res (arg `LamCtx_TermS` c)
147 Token_Term_App tok_lam tok_arg_actual ->
148 compileO tok_lam ctx $ \ty_lam (TermO lam_) ->
149 compileO tok_arg_actual ctx $ \ty_arg_actual (TermO arg_actual) ->
150 check_TyEq2 (ty @(->)) (At (Just tok_lam) ty_lam) $ \Refl ty_arg ty_res ->
151 check_TyEq
152 (At (Just tok_lam) ty_arg)
153 (At (Just tok_arg_actual) ty_arg_actual) $ \Refl ->
154 k ty_res $ TermO $
155 \c -> lam_ c .$ arg_actual c
156 Token_Term_Let name tok_bound tok_body ->
157 compileO tok_bound ctx $ \ty_bound (TermO bound) ->
158 compileO tok_body (LamCtx_TypeS name ty_bound ctx) $
159 \ty_res (TermO res) ->
160 k ty_res $ TermO $
161 \c -> let_ (bound c) $ \arg -> res (arg `LamCtx_TermS` c)
162 Token_Term_Var nam -> go nam ctx k
163 where
164 go :: forall meta lc ret ls rs.
165 Term_Name
166 -> LamCtx_Type is Term_Name lc
167 -> ( forall h.
168 Type (TyConsts_of_Ifaces is) (h::Kind.Type)
169 -> TermO lc h is ls rs
170 -> Either (Error_Term meta is) ret )
171 -> Either (Error_Term meta is) ret
172 go name lc k' =
173 case lc of
174 LamCtx_TypeZ -> Left $ Error_Term_unbound name
175 LamCtx_TypeS n typ _ | n == name ->
176 k' typ $ TermO $ \(te `LamCtx_TermS` _) -> te
177 LamCtx_TypeS _n _ty lc' ->
178 go name lc' $ \typ (TermO te::TermO lc' h is '[] is) ->
179 k' typ $ TermO $ \(_ `LamCtx_TermS` c) -> te c
180 Token_Term_Compose tok_f tok_g ->
181 -- (.) :: (b -> c) -> (a -> b) -> a -> c
182 compileO tok_f ctx $ \ty_f (TermO f) ->
183 compileO tok_g ctx $ \ty_g (TermO g) ->
184 check_TyEq2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_b ty_c ->
185 check_TyEq2 (ty @(->)) (At (Just tok_g) ty_g) $ \Refl ty_a ty_g_b ->
186 check_TyEq
187 (At (Just tok_f) ty_f_b)
188 (At (Just tok_g) ty_g_b) $ \Refl ->
189 k (ty_a ~> ty_c) $ TermO $
190 \c -> (^) (f c) (g c)
191 instance
192 Inj_Token meta ts (->) =>
193 TokenizeT meta ts (Proxy (->)) where
194 tokenizeT _t = mempty
195 { tokenizers_infix = tokenizeTMod []
196 [ tokenize2 "." (infixR 9) Token_Term_Compose
197 , tokenize2 "$" (infixR 0) Token_Term_App
198 ]
199 }
200 instance Gram_Term_AtomsT meta ts (Proxy (->)) g
201
202 -- | The function 'Type' @(->)@,
203 -- with an infix notation more readable.
204 (~>) :: forall cs a b. Inj_TyConst cs (->)
205 => Type cs a -> Type cs b -> Type cs (a -> b)
206 (~>) a b = ty @(->) :$ a :$ b
207 infixr 5 ~>