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 (Proxy 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 FixityOf Monad
  62 instance ClassInstancesFor Monad
  63 instance TypeInstancesFor Monad
  64
  65 -- Compiling
  66 instance Gram_Term_AtomsFor src ss g Monad
  67 instance (Source src, Inj_Sym ss Monad) => ModuleFor src ss Monad where
  68         moduleFor _s = ["Monad"] `moduleWhere`
  69          [ "return" := teMonad_return
  70          , "join"   := teMonad_join
  71          , "when"   := teMonad_when
  72          , ">>=" `withInfixL` 1 := teMonad_bind
  73          , ">=>" `withInfixR` 1 := teMonad_kleisli_l2r
  74          ]
  75
  76 -- ** 'Type's
  77 tyMonad :: Source src => Type src vs m -> Type src vs (Monad m)
  78 tyMonad m = tyConstLen @(K Monad) @Monad (lenVars m) `tyApp` m
  79
  80 m0 :: Source src => Inj_Len vs => Inj_Kind (K m) =>
  81      Type src (Proxy m ': vs) m
  82 m0 = tyVar "m" varZ
  83
  84 m1 :: Source src => Inj_Len vs => Inj_Kind (K m) =>
  85      Type src (a ': Proxy m ': vs) m
  86 m1 = tyVar "m" $ VarS varZ
  87
  88 m2 :: Source src => Inj_Len vs => Inj_Kind (K m) =>
  89      Type src (a ': b ': Proxy m ': vs) m
  90 m2 = tyVar "m" $ VarS $ VarS varZ
  91
  92 m3 :: Source src => Inj_Len vs => Inj_Kind (K m) =>
  93      Type src (a ': b ': c ': Proxy m ': vs) m
  94 m3 = tyVar "m" $ VarS $ VarS $ VarS varZ
  95
  96 -- ** 'Term's
  97 teMonad_return :: TermDef Monad '[Proxy a, Proxy m] (Monad m #> (a -> m a))
  98 teMonad_return = Term (tyMonad m1) (a0 ~> m1 `tyApp` a0) $ teSym @Monad $ lam1 return
  99
 100 teMonad_bind :: TermDef Monad '[Proxy a, Proxy b, Proxy m] (Monad m #> (m a -> (a -> m b) -> m b))
 101 teMonad_bind = Term (tyMonad m2) (m2 `tyApp` a0 ~> (a0 ~> m2 `tyApp` b1) ~> m2 `tyApp` b1) $ teSym @Monad $ lam2 (>>=)
 102
 103 teMonad_join :: TermDef Monad '[Proxy a, Proxy m] (Monad m #> (m (m a) -> m a))
 104 teMonad_join = Term (tyMonad m1) (m1 `tyApp` (m1 `tyApp` a0) ~> m1 `tyApp` a0) $ teSym @Monad $ lam1 join
 105
 106 teMonad_kleisli_l2r :: TermDef Monad '[Proxy a, Proxy b, Proxy c, Proxy m] (Monad m #> ((a -> m b) -> (b -> m c) -> (a -> m c)))
 107 teMonad_kleisli_l2r = Term (tyMonad m3) ((a0 ~> m3 `tyApp` b1) ~> (b1 ~> m3 `tyApp` c2) ~> (a0 ~> m3 `tyApp` c2)) $ teSym @Monad $ lam2 (>=>)
 108
 109 teMonad_when :: TermDef Monad '[Proxy m] (Monad m #> (Bool -> m () -> m ()))
 110 teMonad_when = Term (tyMonad m0) (tyBool ~> m0 `tyApp` tyUnit ~> m0 `tyApp` tyUnit) $ teSym @Monad $ lam2 when