Language/Symantic/Expr/Monad.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE Rank2Types #-}
   7 {-# LANGUAGE ScopedTypeVariables #-}
   8 {-# LANGUAGE TypeFamilies #-}
   9 {-# LANGUAGE TypeOperators #-}
  10 {-# OPTIONS_GHC -fno-warn-orphans #-}
  11 -- | Expression for 'Monad'.
  12 module Language.Symantic.Expr.Monad where
  13
  14 import Control.Monad (Monad)
  15 import qualified Data.Function as Fun
  16 import Data.Proxy (Proxy(..))
  17 import Data.Type.Equality ((:~:)(Refl))
  18 import Prelude hiding ((<$>), Monad(..))
  19
  20 import Language.Symantic.Type
  21 import Language.Symantic.Trans.Common
  22 import Language.Symantic.Expr.Root
  23 import Language.Symantic.Expr.Error
  24 import Language.Symantic.Expr.From
  25 import Language.Symantic.Expr.Lambda
  26 import Language.Symantic.Expr.Functor
  27
  28 -- * Class 'Sym_Monad'
  29 -- | Symantic.
  30 class Sym_Functor repr => Sym_Monad repr where
  31         return :: Monad m => repr a -> repr (m a)
  32         (>>=)  :: Monad m => repr (m a) -> repr ((->) a (m b)) -> repr (m b)
  33
  34         default return :: (Trans t repr, Monad m)
  35          => t repr a -> t repr (m a)
  36         default (>>=) :: (Trans t repr, Monad m)
  37          => t repr (m a) -> t repr ((->) a (m b)) -> t repr (m b)
  38
  39         return = trans_map1 return
  40         (>>=)  = trans_map2 (>>=)
  41 infixl 1 >>=
  42
  43 -- * Type 'Expr_Monad'
  44 -- | Expression.
  45 data Expr_Monad (root:: *)
  46 type instance Root_of_Expr      (Expr_Monad root)      = root
  47 type instance Type_of_Expr      (Expr_Monad root)      = No_Type
  48 type instance Sym_of_Expr       (Expr_Monad root) repr = (Sym_Monad repr)
  49 type instance Error_of_Expr ast (Expr_Monad root)      = No_Error_Expr
  50
  51 return_from
  52  :: forall root ty ast hs ret.
  53  ( ty ~ Type_Root_of_Expr (Expr_Monad root)
  54  , Eq_Type ty
  55  , Type1_from ast ty
  56  , Expr_from ast root
  57  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  58                    (Error_of_Expr ast root)
  59  , Root_of_Expr root ~ root
  60  , Constraint_Type1 Monad ty
  61  ) => ast -> ast
  62  -> Expr_From ast (Expr_Monad root) hs ret
  63 return_from ast_f ast_a ex ast ctx k =
  64  -- return :: Monad f => a -> f a
  65         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) Fun.id $
  66         type1_from (Proxy::Proxy ty) ast_f $ \_f ty_f -> Right $
  67                 expr_from (Proxy::Proxy root) ast_a ctx $
  68                  \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
  69                 let ty_fa = ty_f ty_a in
  70                 check_constraint_type1 ex (Proxy::Proxy Monad) ast ty_fa $ \Dict ->
  71                 k ty_fa $ Forall_Repr_with_Context $
  72                  \c -> return (a c)
  73
  74 bind_from
  75  :: forall root ty ast hs ret.
  76  ( ty ~ Type_Root_of_Expr (Expr_Monad root)
  77  , Eq_Type ty
  78  , Eq_Type1 ty
  79  , Expr_from ast root
  80  , Lift_Type   Type_Fun (Type_of_Expr root)
  81  , Unlift_Type Type_Fun (Type_of_Expr root)
  82  , Unlift_Type1 (Type_of_Expr root)
  83  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  84                    (Error_of_Expr ast root)
  85  , Root_of_Expr root ~ root
  86  , Constraint_Type1 Monad ty
  87  ) => ast -> ast
  88  -> Expr_From ast (Expr_Monad root) hs ret
  89 bind_from ast_ma ast_f ex ast ctx k =
  90  -- (>>=) :: Monad m => m a -> (a -> m b) -> m b
  91         expr_from (Proxy::Proxy root) ast_ma ctx $
  92          \(ty_ma::ty h_ma) (Forall_Repr_with_Context ma) ->
  93         expr_from (Proxy::Proxy root) ast_f ctx $
  94          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
  95         check_type1 ex ast ty_ma $ \(Type_Type1 m ty_m_a, Lift_Type1 ty_m) ->
  96         check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_mb
  97          :: Type_Fun ty h_f) ->
  98         check_eq_type ex ast ty_m_a ty_f_a $ \Refl ->
  99         check_type1 ex ast ty_f_mb $ \(Type_Type1 _ ty_f_m_b, _) ->
 100         check_eq_type1 ex ast ty_ma ty_f_mb $ \Refl ->
 101         check_constraint_type1 ex (Proxy::Proxy Monad) ast ty_ma $ \Dict ->
 102         k (Type_Root $ ty_m $ Type_Type1 m ty_f_m_b) $ Forall_Repr_with_Context $
 103          \c -> (>>=) (ma c) (f c)