symantic-lib/Language/Symantic/Lib/Monad.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Monad'.
   4 module Language.Symantic.Lib.Monad where
   5
   6 import Control.Monad (Monad)
   7 import Data.Proxy
   8 import Data.Type.Equality ((:~:)(Refl))
   9 import Prelude hiding (Monad(..))
  10 import qualified Control.Monad as Monad
  11
  12 import Language.Symantic.Parsing
  13 import Language.Symantic.Typing
  14 import Language.Symantic.Compiling
  15 import Language.Symantic.Interpreting
  16 import Language.Symantic.Transforming
  17 import Language.Symantic.Lib.Lambda ((~>))
  18 import Language.Symantic.Lib.Applicative (Sym_Applicative)
  19
  20 -- * Class 'Sym_Monad'
  21 class Sym_Applicative term => Sym_Monad term where
  22         return :: Monad m => term a -> term (m a)
  23         (>>=)  :: Monad m => term (m a) -> term (a -> m b) -> term (m b); infixl 1 >>=
  24         join   :: Monad m => term (m (m a)) -> term (m a)
  25         when   :: Applicative f => term Bool -> term (f ()) -> term (f ())
  26         (>=>)  :: Monad m => term (a -> m b) -> term (b -> m c) -> term (a -> m c); infixr 1 >=>
  27
  28         default return :: (Trans t term, Monad m) => t term a -> t term (m a)
  29         default (>>=)  :: (Trans t term, Monad m) => t term (m a) -> t term (a -> m b) -> t term (m b)
  30         default join   :: (Trans t term, Monad m) => t term (m (m a)) -> t term (m a)
  31         default when   :: (Trans t term, Applicative f) => t term Bool -> t term (f ()) -> t term (f ())
  32         default (>=>)  :: (Trans t term, Monad m) => t term (a -> m b) -> t term (b -> m c) -> t term (a -> m c)
  33
  34         return = trans_map1 return
  35         (>>=)  = trans_map2 (>>=)
  36         join   = trans_map1 join
  37         when   = trans_map2 when
  38         (>=>)  = trans_map2 (>=>)
  39
  40 type instance Sym_of_Iface (Proxy Monad) = Sym_Monad
  41 type instance TyConsts_of_Iface (Proxy Monad) = Proxy Monad ': TyConsts_imported_by (Proxy Monad)
  42 type instance TyConsts_imported_by (Proxy Monad) =
  43  [ Proxy ()
  44  , Proxy Applicative
  45  , Proxy Bool
  46  ]
  47
  48 instance Sym_Monad HostI where
  49         return = Monad.liftM  Monad.return
  50         (>>=)  = Monad.liftM2 (Monad.>>=)
  51         join   = Monad.liftM  Monad.join
  52         when   = Monad.liftM2 Monad.when
  53         (>=>)  = Monad.liftM2 (Monad.>=>)
  54 instance Sym_Monad TextI where
  55         return = textI1 "return"
  56         (>>=)  = textI_infix ">>=" (infixL 1)
  57         join   = textI1 "join"
  58         when   = textI2 "when"
  59         (>=>)  = textI_infix ">=>" (infixR 1)
  60 instance (Sym_Monad r1, Sym_Monad r2) => Sym_Monad (DupI r1 r2) where
  61         return = dupI1 @Sym_Monad return
  62         (>>=)  = dupI2 @Sym_Monad (>>=)
  63         join   = dupI1 @Sym_Monad join
  64         when   = dupI2 @Sym_Monad when
  65         (>=>)  = dupI2 @Sym_Monad (>=>)
  66
  67 instance
  68  ( Read_TyNameR TyName cs rs
  69  , Inj_TyConst cs Monad
  70  ) => Read_TyNameR TyName cs (Proxy Monad ': rs) where
  71         read_TyNameR _cs (TyName "Monad") k = k (ty @Monad)
  72         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  73 instance Show_TyConst cs => Show_TyConst (Proxy Monad ': cs) where
  74         show_TyConst TyConstZ{} = "Monad"
  75         show_TyConst (TyConstS c) = show_TyConst c
  76
  77 instance Proj_TyConC cs (Proxy Monad)
  78 data instance TokenT meta (ts::[*]) (Proxy Monad)
  79  = Token_Term_Monad_return      (EToken meta '[Proxy Token_Type]) (EToken meta ts)
  80  | Token_Term_Monad_bind        (EToken meta ts) (EToken meta ts)
  81  | Token_Term_Monad_join        (EToken meta ts)
  82  | Token_Term_Monad_when        (EToken meta ts) (EToken meta ts)
  83  | Token_Term_Monad_kleisli_l2r (EToken meta ts) (EToken meta ts)
  84 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Monad))
  85 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Monad))
  86
  87 instance -- CompileI
  88  ( Read_TyName TyName cs
  89  , Inj_TyConst cs Monad
  90  , Inj_TyConst cs (->)
  91  , Inj_TyConst cs ()
  92  , Inj_TyConst cs Applicative
  93  , Inj_TyConst cs Bool
  94  , Proj_TyCon cs
  95  , Compile cs is
  96  ) => CompileI cs is (Proxy Monad) where
  97         compileI tok ctx k =
  98                 case tok of
  99                  Token_Term_Monad_return tok_ty_m tok_a ->
 100                         -- return :: Monad m => a -> m a
 101                         compile_Type tok_ty_m $ \(ty_m::Type cs m) ->
 102                         check_Kind
 103                          (At Nothing (SKiType `SKiArrow` SKiType))
 104                          (At (Just tok_ty_m) $ kind_of ty_m) $ \Refl ->
 105                         check_TyCon (At (Just tok_ty_m) (ty @Monad :$ ty_m)) $ \TyCon ->
 106                         compile tok_a ctx $ \ty_a (Term a) ->
 107                         k (ty_m :$ ty_a) $ Term $
 108                          \c -> return (a c)
 109                  Token_Term_Monad_bind tok_ma tok_a2mb ->
 110                         -- (>>=) :: Monad m => m a -> (a -> m b) -> m b
 111                         compile tok_ma   ctx $ \ty_ma   (Term ma) ->
 112                         compile tok_a2mb ctx $ \ty_a2mb (Term a2mb) ->
 113                         check_TyCon1 (ty @Monad) (At (Just tok_ma) ty_ma) $ \Refl TyCon ty_ma_m ty_ma_a ->
 114                         check_TyEq2 (ty @(->)) (At (Just tok_a2mb) ty_a2mb) $ \Refl ty_a2mb_a ty_a2mb_mb ->
 115                         check_TyEq1 ty_ma_m (At (Just tok_a2mb) ty_a2mb_mb) $ \Refl _ty_a2mb_mb_b ->
 116                         check_TyEq
 117                          (At (Just tok_a2mb) ty_a2mb_a)
 118                          (At (Just tok_ma) ty_ma_a) $ \Refl ->
 119                         k ty_a2mb_mb $ Term $
 120                          \c -> (>>=) (ma c) (a2mb c)
 121                  Token_Term_Monad_join tok_mma ->
 122                         -- join :: Monad m => m (m a) -> m a
 123                         compile tok_mma ctx $ \ty_mma (Term mma) ->
 124                         check_TyCon1 (ty @Monad) (At (Just tok_mma) ty_mma) $ \Refl TyCon ty_mma_m ty_mma_ma ->
 125                         check_TyEq1 ty_mma_m (At (Just tok_mma) ty_mma_ma) $ \Refl _ty_mma_ma_a ->
 126                         k ty_mma_ma $ Term $
 127                          \c -> join (mma c)
 128                  Token_Term_Monad_when tok_cond tok_ok ->
 129                         -- when :: Applicative f => Bool -> f () -> f ()
 130                         compile tok_cond ctx $ \ty_cond (Term cond) ->
 131                         compile tok_ok   ctx $ \ty_ok   (Term ok) ->
 132                         check_TyCon1 (ty @Applicative) (At (Just tok_ok) ty_ok) $ \Refl TyCon _ty_ok_f ty_ok_u ->
 133                         check_TyEq
 134                          (At Nothing (ty @Bool))
 135                          (At (Just tok_cond) ty_cond) $ \Refl ->
 136                         check_TyEq
 137                          (At Nothing (ty @()))
 138                          (At (Just tok_ok) ty_ok_u) $ \Refl ->
 139                         k ty_ok $ Term $
 140                          \c -> when (cond c) (ok c)
 141                  Token_Term_Monad_kleisli_l2r tok_a2mb tok_b2mc ->
 142                         -- (>=>) :: Monad m => (a -> m b) -> (b -> m c) -> a -> m c
 143                         compile tok_a2mb ctx $ \ty_a2mb (Term a2mb) ->
 144                         compile tok_b2mc ctx $ \ty_b2mc (Term b2mc) ->
 145                         check_TyEq2 (ty @(->)) (At (Just tok_a2mb) ty_a2mb) $ \Refl ty_a2mb_a ty_a2mb_mb ->
 146                         check_TyEq2 (ty @(->)) (At (Just tok_b2mc) ty_b2mc) $ \Refl ty_b2mc_b ty_b2mc_mc ->
 147                         check_TyCon1 (ty @Monad) (At (Just tok_a2mb) ty_a2mb_mb) $ \Refl TyCon ty_a2mb_mb_m ty_a2mb_mb_b ->
 148                         check_TyEq1 ty_a2mb_mb_m (At (Just tok_b2mc) ty_b2mc_mc) $ \Refl _ty_b2mc_mc_c ->
 149                         check_TyEq1 ty_a2mb_mb_m (At (Just tok_a2mb) ty_a2mb_mb) $ \Refl _ty_a2mb_mb_b ->
 150                         check_TyEq
 151                          (At (Just tok_a2mb) ty_a2mb_mb_b)
 152                          (At (Just tok_b2mc) ty_b2mc_b) $ \Refl ->
 153                         k (ty_a2mb_a ~> ty_b2mc_mc) $ Term $
 154                          \c -> (>=>) (a2mb c) (b2mc c)
 155 instance -- TokenizeT
 156  Inj_Token meta ts Monad =>
 157  TokenizeT meta ts (Proxy Monad) where
 158         tokenizeT _t = mempty
 159          { tokenizers_infix = tokenizeTMod []
 160                  [ (TeName "Nothing",) ProTok_Term
 161                          { protok_term = \meta -> ProTokPi $ \m -> ProTokLam $ \a ->
 162                                 ProTokTe $ inj_EToken meta $ Token_Term_Monad_return m a
 163                          , protok_fixity = infixN5
 164                          }
 165                  , tokenize2 ">>="  (infixL 1) Token_Term_Monad_bind
 166                  , tokenize1 "join" infixN5    Token_Term_Monad_join
 167                  , tokenize2 "when" infixN5    Token_Term_Monad_when
 168                  , tokenize2 ">=>"  (infixR 1) Token_Term_Monad_kleisli_l2r
 169                  ]
 170          }
 171 instance Gram_Term_AtomsT meta ts (Proxy Monad) g