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
  31  ( Sym_Monad_Lam (Lambda_from_Repr repr) repr
  32  ) => Sym_Monad repr where
  33         return :: Monad f => repr a -> repr (f a)
  34         default return :: (Trans t repr, Monad f) => t repr a -> t repr (f a)
  35         return = trans_map1 return
  36
  37 -- * Class 'Sym_Monad_Lam'
  38 -- | Symantic requiring a 'Lambda'.
  39 class Sym_Functor lam repr => Sym_Monad_Lam lam repr where
  40         (>>=) :: Monad m => repr (m a) -> repr (Lambda lam a (m b)) -> repr (m b)
  41         default (>>=) :: (Trans t repr, Monad m)
  42          => t repr (m a) -> t repr (Lambda lam a (m b)) -> t repr (m b)
  43         (>>=) = trans_map2 (>>=)
  44 infixl 1 >>=
  45
  46 -- * Type 'Expr_Monad'
  47 -- | Expression.
  48 data Expr_Monad (lam:: * -> *) (root:: *)
  49 type instance Root_of_Expr      (Expr_Monad lam root)      = root
  50 type instance Type_of_Expr      (Expr_Monad lam root)      = No_Type
  51 type instance Sym_of_Expr       (Expr_Monad lam root) repr = (Sym_Monad repr, Sym_Monad_Lam lam repr)
  52 type instance Error_of_Expr ast (Expr_Monad lam root)      = No_Error_Expr
  53 instance Constraint_Type1 Monad (Type_Type0 px root)
  54 instance Constraint_Type1 Monad (Type_Var1 root)
  55
  56 return_from
  57  :: forall root ty ty_root lam ast hs ret.
  58  ( ty ~ Type_Root_of_Expr (Expr_Monad lam root)
  59  , ty_root ~ Type_Root_of_Expr root
  60  , Eq_Type (Type_Root_of_Expr root)
  61  , Type1_from ast (Type_Root_of_Expr root)
  62  , Expr_from ast root
  63  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  64                    (Error_of_Expr ast root)
  65  , Root_of_Expr root ~ root
  66  , Constraint_Type1 Monad ty
  67  ) => ast -> ast
  68  -> Expr_From ast (Expr_Monad lam root) hs ret
  69 return_from ast_f ast_a ex ast ctx k =
  70  -- return :: Monad f => a -> f a
  71         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $
  72         type1_from (Proxy::Proxy ty_root) ast_f $ \_f ty_f -> Right $
  73                 expr_from (Proxy::Proxy root) ast_a ctx $
  74                  \(ty_a::Type_Root_of_Expr root h_a) (Forall_Repr_with_Context a) ->
  75                 let ty_fa = ty_f ty_a in
  76                 check_constraint_type1 ex (Proxy::Proxy Monad) ast ty_fa $ \Dict ->
  77                 k ty_fa $ Forall_Repr_with_Context $
  78                  \c -> return (a c)
  79
  80 bind_from
  81  :: forall root ty lam ast hs ret.
  82  ( ty ~ Type_Root_of_Expr (Expr_Monad lam root)
  83  , Eq_Type (Type_Root_of_Expr root)
  84  , Eq_Type1 (Type_Root_of_Expr root)
  85  , Expr_from ast root
  86  , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
  87  , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
  88  , Unlift_Type1 (Type_of_Expr root)
  89  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  90                    (Error_of_Expr ast root)
  91  , Root_of_Expr root ~ root
  92  , Constraint_Type1 Monad ty
  93  ) => ast -> ast
  94  -> Expr_From ast (Expr_Monad lam root) hs ret
  95 bind_from ast_ma ast_f ex ast ctx k =
  96  -- (>>=) :: Monad m => m a -> (a -> m b) -> m b
  97         expr_from (Proxy::Proxy root) ast_ma ctx $
  98          \(ty_ma::Type_Root_of_Expr root h_ma) (Forall_Repr_with_Context ma) ->
  99         expr_from (Proxy::Proxy root) ast_f ctx $
 100          \(ty_f::Type_Root_of_Expr root h_f) (Forall_Repr_with_Context f) ->
 101         check_type1 ex ast ty_ma $ \(Type_Type1 m ty_m_a, Lift_Type1 ty_m) ->
 102         check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_mb
 103          :: Type_Fun lam (Type_Root_of_Expr root) h_f) ->
 104         check_eq_type ex ast ty_m_a ty_f_a $ \Refl ->
 105         check_type1 ex ast ty_f_mb $ \(Type_Type1 _ ty_f_m_b, _) ->
 106         check_eq_type1 ex ast ty_ma ty_f_mb $ \Refl ->
 107         check_constraint_type1 ex (Proxy::Proxy Monad) ast ty_ma $ \Dict ->
 108         k (Type_Root $ ty_m $ Type_Type1 m ty_f_m_b) $ Forall_Repr_with_Context $
 109          \c -> (>>=) (ma c) (f c)