+{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Monad'.
module Language.Symantic.Lib.Monad where
import Control.Monad (Monad)
-import qualified Control.Monad as Monad
-import Data.Proxy
-import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (Monad(..))
+import qualified Control.Monad as Monad
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
-import Language.Symantic.Lib.Applicative (Sym_Applicative)
+import Language.Symantic
+import Language.Symantic.Lib.Function (a0, b1, c2)
+import Language.Symantic.Lib.Unit (tyUnit)
+import Language.Symantic.Lib.Bool (tyBool)
-- * Class 'Sym_Monad'
-class Sym_Applicative term => Sym_Monad term where
- return :: Monad m => term a -> term (m a)
- (>>=) :: Monad m => term (m a) -> term (a -> m b) -> term (m b); infixl 1 >>=
- join :: Monad m => term (m (m a)) -> term (m a)
+type instance Sym Monad = Sym_Monad
+class Sym_Monad term where
+ return :: Monad m => term a -> term (m a)
+ (>>=) :: Monad m => term (m a) -> term (a -> m b) -> term (m b); infixl 1 >>=
+ join :: Monad m => term (m (m a)) -> term (m a)
when :: Applicative f => term Bool -> term (f ()) -> term (f ())
+ (>=>) :: Monad m => term (a -> m b) -> term (b -> m c) -> term (a -> m c); infixr 1 >=>
- default return :: (Trans t term, Monad m)
- => t term a -> t term (m a)
- default (>>=) :: (Trans t term, Monad m)
- => t term (m a) -> t term (a -> m b) -> t term (m b)
- default join :: (Trans t term, Monad m)
- => t term (m (m a)) -> t term (m a)
- default when :: (Trans t term, Applicative f)
- => t term Bool -> t term (f ()) -> t term (f ())
+ default return :: Sym_Monad (UnT term) => Trans term => Monad m => term a -> term (m a)
+ default (>>=) :: Sym_Monad (UnT term) => Trans term => Monad m => term (m a) -> term (a -> m b) -> term (m b)
+ default join :: Sym_Monad (UnT term) => Trans term => Monad m => term (m (m a)) -> term (m a)
+ default when :: Sym_Monad (UnT term) => Trans term => Applicative f => term Bool -> term (f ()) -> term (f ())
+ default (>=>) :: Sym_Monad (UnT term) => Trans term => Monad m => term (a -> m b) -> term (b -> m c) -> term (a -> m c)
- return = trans_map1 return
- (>>=) = trans_map2 (>>=)
- join = trans_map1 join
- when = trans_map2 when
-
-type instance Sym_of_Iface (Proxy Monad) = Sym_Monad
-type instance TyConsts_of_Iface (Proxy Monad) = Proxy Monad ': TyConsts_imported_by Monad
-type instance TyConsts_imported_by Monad =
- [ Proxy ()
- , Proxy Applicative
- , Proxy Bool
- ]
-
-instance Sym_Monad HostI where
- return = Monad.liftM Monad.return
- (>>=) = Monad.liftM2 (Monad.>>=)
- join = Monad.liftM Monad.join
- when = Monad.liftM2 Monad.when
-instance Sym_Monad TextI where
- return = textI1 "return"
- (>>=) = textI_infix ">>=" (infixL 1)
- join = textI1 "join"
- when = textI2 "when"
-instance (Sym_Monad r1, Sym_Monad r2) => Sym_Monad (DupI r1 r2) where
- return = dupI1 @Sym_Monad return
- (>>=) = dupI2 @Sym_Monad (>>=)
- join = dupI1 @Sym_Monad join
- when = dupI2 @Sym_Monad when
-
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs Monad
- ) => Read_TyNameR TyName cs (Proxy Monad ': rs) where
- read_TyNameR _cs (TyName "Monad") k = k (ty @Monad)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy Monad ': cs) where
- show_TyConst TyConstZ{} = "Monad"
- show_TyConst (TyConstS c) = show_TyConst c
-
-instance Proj_TyConC cs (Proxy Monad)
-data instance TokenT meta (ts::[*]) (Proxy Monad)
- = Token_Term_Monad_return (EToken meta '[Proxy Token_Type]) (EToken meta ts)
- | Token_Term_Monad_bind (EToken meta ts) (EToken meta ts)
- | Token_Term_Monad_join (EToken meta ts)
- | Token_Term_Monad_when (EToken meta ts) (EToken meta ts)
-deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Monad))
-deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Monad))
-instance -- CompileI
- ( Read_TyName TyName cs
- , Inj_TyConst cs Monad
- , Inj_TyConst cs (->)
- , Inj_TyConst cs ()
- , Inj_TyConst cs Applicative
- , Inj_TyConst cs Bool
- , Proj_TyCon cs
- , Compile cs is
- ) => CompileI cs is (Proxy Monad) where
- compileI tok ctx k =
- case tok of
- Token_Term_Monad_return tok_ty_m tok_a ->
- -- return :: Monad m => a -> m a
- compile_Type tok_ty_m $ \(ty_m::Type cs m) ->
- check_Kind
- (At Nothing (SKiType `SKiArrow` SKiType))
- (At (Just tok_ty_m) $ kind_of ty_m) $ \Refl ->
- check_TyCon (At (Just tok_ty_m) (ty @Monad :$ ty_m)) $ \TyCon ->
- compileO tok_a ctx $ \ty_a (TermO a) ->
- k (ty_m :$ ty_a) $ TermO $
- \c -> return (a c)
- Token_Term_Monad_bind tok_ma tok_a2mb ->
- -- (>>=) :: Monad m => m a -> (a -> m b) -> m b
- compileO tok_ma ctx $ \ty_ma (TermO ma) ->
- compileO tok_a2mb ctx $ \ty_a2mb (TermO a2mb) ->
- check_TyCon1 (ty @Monad) (At (Just tok_ma) ty_ma) $ \Refl TyCon ty_ma_m ty_ma_a ->
- check_TyEq2 (ty @(->)) (At (Just tok_a2mb) ty_a2mb) $ \Refl ty_a2mb_a ty_a2mb_mb ->
- check_TyEq1 ty_ma_m (At (Just tok_a2mb) ty_a2mb_mb) $ \Refl _ty_a2mb_mb_b ->
- check_TyEq
- (At (Just tok_a2mb) ty_a2mb_a)
- (At (Just tok_ma) ty_ma_a) $ \Refl ->
- k ty_a2mb_mb $ TermO $
- \c -> (>>=) (ma c) (a2mb c)
- Token_Term_Monad_join tok_mma ->
- -- join :: Monad m => m (m a) -> m a
- compileO tok_mma ctx $ \ty_mma (TermO mma) ->
- check_TyCon1 (ty @Monad) (At (Just tok_mma) ty_mma) $ \Refl TyCon ty_mma_m ty_mma_ma ->
- check_TyEq1 ty_mma_m (At (Just tok_mma) ty_mma_ma) $ \Refl _ty_mma_ma_a ->
- k ty_mma_ma $ TermO $
- \c -> join (mma c)
- Token_Term_Monad_when tok_cond tok_ok ->
- -- when :: Applicative f => Bool -> f () -> f ()
- compileO tok_cond ctx $ \ty_cond (TermO cond) ->
- compileO tok_ok ctx $ \ty_ok (TermO ok) ->
- check_TyCon1 (ty @Applicative) (At (Just tok_ok) ty_ok) $ \Refl TyCon _ty_ok_f ty_ok_u ->
- check_TyEq
- (At Nothing (ty @Bool))
- (At (Just tok_cond) ty_cond) $ \Refl ->
- check_TyEq
- (At Nothing (ty @()))
- (At (Just tok_ok) ty_ok_u) $ \Refl ->
- k ty_ok $ TermO $
- \c -> when (cond c) (ok c)
-instance -- TokenizeT
- Inj_Token meta ts Monad =>
- TokenizeT meta ts (Proxy Monad) where
- tokenizeT _t = mempty
- { tokenizers_infix = tokenizeTMod []
- [ (Term_Name "Nothing",) Term_ProTok
- { term_protok = \meta -> ProTokPi $ \m -> ProTokLam $ \a ->
- ProTok $ inj_EToken meta $ Token_Term_Monad_return m a
- , term_fixity = infixN5
- }
- , tokenize2 ">>=" (infixL 1) Token_Term_Monad_bind
- , tokenize1 "join" infixN5 Token_Term_Monad_join
- , tokenize2 "when" infixN5 Token_Term_Monad_when
- ]
- }
-instance Gram_Term_AtomsT meta ts (Proxy Monad) g
+ return = trans1 return
+ (>>=) = trans2 (>>=)
+ join = trans1 join
+ when = trans2 when
+ (>=>) = trans2 (>=>)
+
+-- Interpreting
+instance Sym_Monad Eval where
+ return = eval1 Monad.return
+ (>>=) = eval2 (Monad.>>=)
+ join = eval1 Monad.join
+ when = eval2 Monad.when
+ (>=>) = eval2 (Monad.>=>)
+instance Sym_Monad View where
+ return = view1 "return"
+ (>>=) = viewInfix ">>=" (infixL 1)
+ join = view1 "join"
+ when = view2 "when"
+ (>=>) = viewInfix ">=>" (infixR 1)
+instance (Sym_Monad r1, Sym_Monad r2) => Sym_Monad (Dup r1 r2) where
+ return = dup1 @Sym_Monad return
+ (>>=) = dup2 @Sym_Monad (>>=)
+ join = dup1 @Sym_Monad join
+ when = dup2 @Sym_Monad when
+ (>=>) = dup2 @Sym_Monad (>=>)
+
+-- Transforming
+instance (Sym_Monad term, Sym_Lambda term) => Sym_Monad (BetaT term)
+
+-- Typing
+instance NameTyOf Monad where
+ nameTyOf _c = ["Monad"] `Mod` "Monad"
+instance FixityOf Monad
+instance ClassInstancesFor Monad
+instance TypeInstancesFor Monad
+
+-- Compiling
+instance Gram_Term_AtomsFor src ss g Monad
+instance (Source src, SymInj ss Monad) => ModuleFor src ss Monad where
+ moduleFor = ["Monad"] `moduleWhere`
+ [ "return" := teMonad_return
+ , "join" := teMonad_join
+ , "when" := teMonad_when
+ , ">>=" `withInfixL` 1 := teMonad_bind
+ , ">=>" `withInfixR` 1 := teMonad_kleisli_l2r
+ ]
+
+-- ** 'Type's
+tyMonad :: Source src => Type src vs m -> Type src vs (Monad m)
+tyMonad m = tyConstLen @(K Monad) @Monad (lenVars m) `tyApp` m
+
+m0 :: Source src => LenInj vs => KindInj (K m) =>
+ Type src (Proxy m ': vs) m
+m0 = tyVar "m" varZ
+
+m1 :: Source src => LenInj vs => KindInj (K m) =>
+ Type src (a ': Proxy m ': vs) m
+m1 = tyVar "m" $ VarS varZ
+
+m2 :: Source src => LenInj vs => KindInj (K m) =>
+ Type src (a ': b ': Proxy m ': vs) m
+m2 = tyVar "m" $ VarS $ VarS varZ
+
+m3 :: Source src => LenInj vs => KindInj (K m) =>
+ Type src (a ': b ': c ': Proxy m ': vs) m
+m3 = tyVar "m" $ VarS $ VarS $ VarS varZ
+
+-- ** 'Term's
+teMonad_return :: TermDef Monad '[Proxy a, Proxy m] (Monad m #> (a -> m a))
+teMonad_return = Term (tyMonad m1) (a0 ~> m1 `tyApp` a0) $ teSym @Monad $ lam1 return
+
+teMonad_bind :: TermDef Monad '[Proxy a, Proxy b, Proxy m] (Monad m #> (m a -> (a -> m b) -> m b))
+teMonad_bind = Term (tyMonad m2) (m2 `tyApp` a0 ~> (a0 ~> m2 `tyApp` b1) ~> m2 `tyApp` b1) $ teSym @Monad $ lam2 (>>=)
+
+teMonad_join :: TermDef Monad '[Proxy a, Proxy m] (Monad m #> (m (m a) -> m a))
+teMonad_join = Term (tyMonad m1) (m1 `tyApp` (m1 `tyApp` a0) ~> m1 `tyApp` a0) $ teSym @Monad $ lam1 join
+
+teMonad_kleisli_l2r :: TermDef Monad '[Proxy a, Proxy b, Proxy c, Proxy m] (Monad m #> ((a -> m b) -> (b -> m c) -> (a -> m c)))
+teMonad_kleisli_l2r = Term (tyMonad m3) ((a0 ~> m3 `tyApp` b1) ~> (b1 ~> m3 `tyApp` c2) ~> (a0 ~> m3 `tyApp` c2)) $ teSym @Monad $ lam2 (>=>)
+
+teMonad_when :: TermDef Monad '[Proxy m] (Monad m #> (Bool -> m () -> m ()))
+teMonad_when = Term (tyMonad m0) (tyBool ~> m0 `tyApp` tyUnit ~> m0 `tyApp` tyUnit) $ teSym @Monad $ lam2 when
sourcephile / git / haskell / symantic.git / blobdiff