]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Expr/Monad.hs
polish code, Foldable
[haskell/symantic.git] / Language / Symantic / Expr / Monad.hs
1 {-# LANGUAGE DefaultSignatures #-}
2 {-# LANGUAGE GADTs #-}
3 {-# LANGUAGE FlexibleContexts #-}
4 {-# LANGUAGE FlexibleInstances #-}
5 {-# LANGUAGE MultiParamTypeClasses #-}
6 {-# LANGUAGE OverloadedStrings #-}
7 {-# LANGUAGE Rank2Types #-}
8 {-# LANGUAGE ScopedTypeVariables #-}
9 {-# LANGUAGE TypeFamilies #-}
10 {-# LANGUAGE TypeOperators #-}
11 {-# OPTIONS_GHC -fno-warn-orphans #-}
12 -- | Expression for 'Monad'.
13 module Language.Symantic.Expr.Monad where
14
15 import Control.Monad (Monad)
16 import qualified Control.Monad as Monad
17 import qualified Data.Function as Fun
18 import Data.Proxy (Proxy(..))
19 import Data.Type.Equality ((:~:)(Refl))
20 import Prelude hiding ((<$>), Monad(..))
21
22 import Language.Symantic.Type
23 import Language.Symantic.Repr
24 import Language.Symantic.Expr.Root
25 import Language.Symantic.Expr.Error
26 import Language.Symantic.Expr.From
27 import Language.Symantic.Expr.Lambda
28 import Language.Symantic.Expr.Functor
29 import Language.Symantic.Trans.Common
30
31 -- * Class 'Sym_Monad'
32 -- | Symantic.
33 class Sym_Functor repr => Sym_Monad repr where
34 return :: Monad m => repr a -> repr (m a)
35 (>>=) :: Monad m => repr (m a) -> repr (a -> m b) -> repr (m b)
36
37 default return :: (Trans t repr, Monad m)
38 => t repr a -> t repr (m a)
39 default (>>=) :: (Trans t repr, Monad m)
40 => t repr (m a) -> t repr (a -> m b) -> t repr (m b)
41
42 return = trans_map1 return
43 (>>=) = trans_map2 (>>=)
44 infixl 1 >>=
45 instance Sym_Monad Repr_Host where
46 return = Monad.liftM Monad.return
47 (>>=) = Monad.liftM2 (Monad.>>=)
48 instance Sym_Monad Repr_Text where
49 return = repr_text_app1 "return"
50 (>>=) = repr_text_infix ">>=" (Precedence 1)
51 instance (Sym_Monad r1, Sym_Monad r2) => Sym_Monad (Repr_Dup r1 r2) where
52 return = repr_dup1 sym_Monad return
53 (>>=) = repr_dup2 sym_Monad (>>=)
54
55 sym_Monad :: Proxy Sym_Monad
56 sym_Monad = Proxy
57
58 -- * Type 'Expr_Monad'
59 -- | Expression.
60 data Expr_Monad (root:: *)
61 type instance Root_of_Expr (Expr_Monad root) = root
62 type instance Type_of_Expr (Expr_Monad root) = No_Type
63 type instance Sym_of_Expr (Expr_Monad root) repr = Sym_Monad repr
64 type instance Error_of_Expr ast (Expr_Monad root) = No_Error_Expr
65
66 return_from
67 :: forall root ty ast hs ret.
68 ( ty ~ Type_Root_of_Expr (Expr_Monad root)
69 , Type0_Eq ty
70 , Type1_From ast ty
71 , Type1_Constraint Monad ty
72 , Expr_From ast root
73 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
74 (Error_of_Expr ast root)
75 , Root_of_Expr root ~ root
76 ) => ast -> ast
77 -> ExprFrom ast (Expr_Monad root) hs ret
78 return_from ast_f ast_a ex ast ctx k =
79 -- return :: Monad f => a -> f a
80 either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) Fun.id $
81 type1_from (Proxy::Proxy ty) ast_f $ \_f ty_f -> Right $
82 expr_from (Proxy::Proxy root) ast_a ctx $
83 \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
84 let ty_fa = ty_f ty_a in
85 check_type1_constraint ex (Proxy::Proxy Monad) ast ty_fa $ \Dict ->
86 k ty_fa $ Forall_Repr_with_Context $
87 \c -> return (a c)
88
89 bind_from
90 :: forall root ty ast hs ret.
91 ( ty ~ Type_Root_of_Expr (Expr_Monad root)
92 , Type0_Eq ty
93 , Type1_Eq ty
94 , Expr_From ast root
95 , Type0_Lift Type_Fun (Type_of_Expr root)
96 , Type0_Unlift Type_Fun (Type_of_Expr root)
97 , Type1_Unlift (Type_of_Expr root)
98 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
99 (Error_of_Expr ast root)
100 , Root_of_Expr root ~ root
101 , Type1_Constraint Monad ty
102 ) => ast -> ast
103 -> ExprFrom ast (Expr_Monad root) hs ret
104 bind_from ast_ma ast_f ex ast ctx k =
105 -- (>>=) :: Monad m => m a -> (a -> m b) -> m b
106 expr_from (Proxy::Proxy root) ast_ma ctx $
107 \(ty_ma::ty h_ma) (Forall_Repr_with_Context ma) ->
108 expr_from (Proxy::Proxy root) ast_f ctx $
109 \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
110 check_type1 ex ast ty_ma $ \(Type1 m ty_m_a, Type1_Lift ty_m) ->
111 check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_mb) ->
112 check_type0_eq ex ast ty_m_a ty_f_a $ \Refl ->
113 check_type1 ex ast ty_f_mb $ \(Type1 _ ty_f_m_b, _) ->
114 check_type1_eq ex ast ty_ma ty_f_mb $ \Refl ->
115 check_type1_constraint ex (Proxy::Proxy Monad) ast ty_ma $ \Dict ->
116 k (Type_Root $ ty_m $ Type1 m ty_f_m_b) $ Forall_Repr_with_Context $
117 \c -> (>>=) (ma c) (f c)