]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Monad.hs
Update to lastest symantic-document
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Monad.hs
1 {-# LANGUAGE PolyKinds #-}
2 {-# LANGUAGE UndecidableInstances #-}
3 {-# OPTIONS_GHC -fno-warn-orphans #-}
4 -- | Symantic for 'Monad'.
5 module Language.Symantic.Lib.Monad where
6
7 import Control.Monad (Monad)
8 import Prelude hiding (Monad(..))
9 import qualified Control.Monad as Monad
10
11 import Language.Symantic
12 import Language.Symantic.Lib.Function (a0, b1, c2)
13 import Language.Symantic.Lib.Unit (tyUnit)
14 import Language.Symantic.Lib.Bool (tyBool)
15
16 -- * Class 'Sym_Monad'
17 type instance Sym Monad = Sym_Monad
18 class Sym_Monad term where
19 return :: Monad m => term a -> term (m a)
20 (>>=) :: Monad m => term (m a) -> term (a -> m b) -> term (m b); infixl 1 >>=
21 join :: Monad m => term (m (m a)) -> term (m a)
22 when :: Applicative f => term Bool -> term (f ()) -> term (f ())
23 (>=>) :: Monad m => term (a -> m b) -> term (b -> m c) -> term (a -> m c); infixr 1 >=>
24
25 default return :: Sym_Monad (UnT term) => Trans term => Monad m => term a -> term (m a)
26 default (>>=) :: Sym_Monad (UnT term) => Trans term => Monad m => term (m a) -> term (a -> m b) -> term (m b)
27 default join :: Sym_Monad (UnT term) => Trans term => Monad m => term (m (m a)) -> term (m a)
28 default when :: Sym_Monad (UnT term) => Trans term => Applicative f => term Bool -> term (f ()) -> term (f ())
29 default (>=>) :: Sym_Monad (UnT term) => Trans term => Monad m => term (a -> m b) -> term (b -> m c) -> term (a -> m c)
30
31 return = trans1 return
32 (>>=) = trans2 (>>=)
33 join = trans1 join
34 when = trans2 when
35 (>=>) = trans2 (>=>)
36
37 -- Interpreting
38 instance Sym_Monad Eval where
39 return = eval1 Monad.return
40 (>>=) = eval2 (Monad.>>=)
41 join = eval1 Monad.join
42 when = eval2 Monad.when
43 (>=>) = eval2 (Monad.>=>)
44 instance Sym_Monad View where
45 return = view1 "return"
46 (>>=) = viewInfix ">>=" (infixL 1)
47 join = view1 "join"
48 when = view2 "when"
49 (>=>) = viewInfix ">=>" (infixR 1)
50 instance (Sym_Monad r1, Sym_Monad r2) => Sym_Monad (Dup r1 r2) where
51 return = dup1 @Sym_Monad return
52 (>>=) = dup2 @Sym_Monad (>>=)
53 join = dup1 @Sym_Monad join
54 when = dup2 @Sym_Monad when
55 (>=>) = dup2 @Sym_Monad (>=>)
56
57 -- Transforming
58 instance (Sym_Monad term, Sym_Lambda term) => Sym_Monad (BetaT term)
59
60 -- Typing
61 instance NameTyOf Monad where
62 nameTyOf _c = ["Monad"] `Mod` "Monad"
63 instance FixityOf Monad
64 instance ClassInstancesFor Monad
65 instance TypeInstancesFor Monad
66
67 -- Compiling
68 instance Gram_Term_AtomsFor src ss g Monad
69 instance (Source src, SymInj ss Monad) => ModuleFor src ss Monad where
70 moduleFor = ["Monad"] `moduleWhere`
71 [ "return" := teMonad_return
72 , "join" := teMonad_join
73 , "when" := teMonad_when
74 , ">>=" `withInfixL` 1 := teMonad_bind
75 , ">=>" `withInfixR` 1 := teMonad_kleisli_l2r
76 ]
77
78 -- ** 'Type's
79 tyMonad :: Source src => Type src vs m -> Type src vs (Monad m)
80 tyMonad m = tyConstLen @(K Monad) @Monad (lenVars m) `tyApp` m
81
82 m0 :: Source src => LenInj vs => KindInj (K m) =>
83 Type src (Proxy m ': vs) m
84 m0 = tyVar "m" varZ
85
86 m1 :: Source src => LenInj vs => KindInj (K m) =>
87 Type src (a ': Proxy m ': vs) m
88 m1 = tyVar "m" $ VarS varZ
89
90 m2 :: Source src => LenInj vs => KindInj (K m) =>
91 Type src (a ': b ': Proxy m ': vs) m
92 m2 = tyVar "m" $ VarS $ VarS varZ
93
94 m3 :: Source src => LenInj vs => KindInj (K m) =>
95 Type src (a ': b ': c ': Proxy m ': vs) m
96 m3 = tyVar "m" $ VarS $ VarS $ VarS varZ
97
98 -- ** 'Term's
99 teMonad_return :: TermDef Monad '[Proxy a, Proxy m] (Monad m #> (a -> m a))
100 teMonad_return = Term (tyMonad m1) (a0 ~> m1 `tyApp` a0) $ teSym @Monad $ lam1 return
101
102 teMonad_bind :: TermDef Monad '[Proxy a, Proxy b, Proxy m] (Monad m #> (m a -> (a -> m b) -> m b))
103 teMonad_bind = Term (tyMonad m2) (m2 `tyApp` a0 ~> (a0 ~> m2 `tyApp` b1) ~> m2 `tyApp` b1) $ teSym @Monad $ lam2 (>>=)
104
105 teMonad_join :: TermDef Monad '[Proxy a, Proxy m] (Monad m #> (m (m a) -> m a))
106 teMonad_join = Term (tyMonad m1) (m1 `tyApp` (m1 `tyApp` a0) ~> m1 `tyApp` a0) $ teSym @Monad $ lam1 join
107
108 teMonad_kleisli_l2r :: TermDef Monad '[Proxy a, Proxy b, Proxy c, Proxy m] (Monad m #> ((a -> m b) -> (b -> m c) -> (a -> m c)))
109 teMonad_kleisli_l2r = Term (tyMonad m3) ((a0 ~> m3 `tyApp` b1) ~> (b1 ~> m3 `tyApp` c2) ~> (a0 ~> m3 `tyApp` c2)) $ teSym @Monad $ lam2 (>=>)
110
111 teMonad_when :: TermDef Monad '[Proxy m] (Monad m #> (Bool -> m () -> m ()))
112 teMonad_when = Term (tyMonad m0) (tyBool ~> m0 `tyApp` tyUnit ~> m0 `tyApp` tyUnit) $ teSym @Monad $ lam2 when