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