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 Control.Monad as Monad
  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 instance Constraint_Type1 Monad (Type_Type0 px root)
  51 instance Constraint_Type1 Monad (Type_Var1 root)
  52
  53 return_from
  54  :: forall root ty ast hs ret.
  55  ( ty ~ Type_Root_of_Expr (Expr_Monad root)
  56  , Eq_Type ty
  57  , Type1_from ast ty
  58  , Expr_from ast root
  59  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  60                    (Error_of_Expr ast root)
  61  , Root_of_Expr root ~ root
  62  , Constraint_Type1 Monad ty
  63  ) => ast -> ast
  64  -> Expr_From ast (Expr_Monad root) hs ret
  65 return_from ast_f ast_a ex ast ctx k =
  66  -- return :: Monad f => a -> f a
  67         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $
  68         type1_from (Proxy::Proxy ty) ast_f $ \_f ty_f -> Right $
  69                 expr_from (Proxy::Proxy root) ast_a ctx $
  70                  \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
  71                 let ty_fa = ty_f ty_a in
  72                 check_constraint_type1 ex (Proxy::Proxy Monad) ast ty_fa $ \Dict ->
  73                 k ty_fa $ Forall_Repr_with_Context $
  74                  \c -> return (a c)
  75
  76 bind_from
  77  :: forall root ty ast hs ret.
  78  ( ty ~ Type_Root_of_Expr (Expr_Monad root)
  79  , Eq_Type ty
  80  , Eq_Type1 ty
  81  , Expr_from ast root
  82  , Lift_Type   Type_Fun (Type_of_Expr root)
  83  , Unlift_Type Type_Fun (Type_of_Expr root)
  84  , Unlift_Type1 (Type_of_Expr root)
  85  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  86                    (Error_of_Expr ast root)
  87  , Root_of_Expr root ~ root
  88  , Constraint_Type1 Monad ty
  89  ) => ast -> ast
  90  -> Expr_From ast (Expr_Monad root) hs ret
  91 bind_from ast_ma ast_f ex ast ctx k =
  92  -- (>>=) :: Monad m => m a -> (a -> m b) -> m b
  93         expr_from (Proxy::Proxy root) ast_ma ctx $
  94          \(ty_ma::ty h_ma) (Forall_Repr_with_Context ma) ->
  95         expr_from (Proxy::Proxy root) ast_f ctx $
  96          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
  97         check_type1 ex ast ty_ma $ \(Type_Type1 m ty_m_a, Lift_Type1 ty_m) ->
  98         check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_mb
  99          :: Type_Fun ty h_f) ->
 100         check_eq_type ex ast ty_m_a ty_f_a $ \Refl ->
 101         check_type1 ex ast ty_f_mb $ \(Type_Type1 _ ty_f_m_b, _) ->
 102         check_eq_type1 ex ast ty_ma ty_f_mb $ \Refl ->
 103         check_constraint_type1 ex (Proxy::Proxy Monad) ast ty_ma $ \Dict ->
 104         k (Type_Root $ ty_m $ Type_Type1 m ty_f_m_b) $ Forall_Repr_with_Context $
 105          \c -> (>>=) (ma c) (f c)