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
  52 instance
  53  ( Sym_Monad r1
  54  , Sym_Monad r2
  55  ) => Sym_Monad (Dup r1 r2) where
  56         return (a1 `Dup` a2) =
  57                 return a1 `Dup` return a2
  58         (>>=) (m1 `Dup` m2) (f1 `Dup` f2) =
  59                 (>>=) m1 f1 `Dup` (>>=) m2 f2
  60
  61 -- * Type 'Expr_Monad'
  62 -- | Expression.
  63 data Expr_Monad (root:: *)
  64 type instance Root_of_Expr      (Expr_Monad root)      = root
  65 type instance Type_of_Expr      (Expr_Monad root)      = No_Type
  66 type instance Sym_of_Expr       (Expr_Monad root) repr = (Sym_Monad repr)
  67 type instance Error_of_Expr ast (Expr_Monad root)      = No_Error_Expr
  68
  69 return_from
  70  :: forall root ty ast hs ret.
  71  ( ty ~ Type_Root_of_Expr (Expr_Monad root)
  72  , Type0_Eq ty
  73  , Type1_From ast ty
  74  , Type1_Constraint Monad ty
  75  , Expr_From ast root
  76  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  77                    (Error_of_Expr ast root)
  78  , Root_of_Expr root ~ root
  79  ) => ast -> ast
  80  -> ExprFrom ast (Expr_Monad root) hs ret
  81 return_from ast_f ast_a ex ast ctx k =
  82  -- return :: Monad f => a -> f a
  83         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) Fun.id $
  84         type1_from (Proxy::Proxy ty) ast_f $ \_f ty_f -> Right $
  85                 expr_from (Proxy::Proxy root) ast_a ctx $
  86                  \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
  87                 let ty_fa = ty_f ty_a in
  88                 check_type1_constraint ex (Proxy::Proxy Monad) ast ty_fa $ \Dict ->
  89                 k ty_fa $ Forall_Repr_with_Context $
  90                  \c -> return (a c)
  91
  92 bind_from
  93  :: forall root ty ast hs ret.
  94  ( ty ~ Type_Root_of_Expr (Expr_Monad root)
  95  , Type0_Eq ty
  96  , Type1_Eq ty
  97  , Expr_From ast root
  98  , Type0_Lift   Type_Fun (Type_of_Expr root)
  99  , Type0_Unlift Type_Fun (Type_of_Expr root)
 100  , Type1_Unlift (Type_of_Expr root)
 101  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 102                    (Error_of_Expr ast root)
 103  , Root_of_Expr root ~ root
 104  , Type1_Constraint Monad ty
 105  ) => ast -> ast
 106  -> ExprFrom ast (Expr_Monad root) hs ret
 107 bind_from ast_ma ast_f ex ast ctx k =
 108  -- (>>=) :: Monad m => m a -> (a -> m b) -> m b
 109         expr_from (Proxy::Proxy root) ast_ma ctx $
 110          \(ty_ma::ty h_ma) (Forall_Repr_with_Context ma) ->
 111         expr_from (Proxy::Proxy root) ast_f ctx $
 112          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 113         check_type1 ex ast ty_ma $ \(Type1 m ty_m_a, Type1_Lift ty_m) ->
 114         check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_mb
 115          :: Type_Fun ty h_f) ->
 116         check_type0_eq ex ast ty_m_a ty_f_a $ \Refl ->
 117         check_type1 ex ast ty_f_mb $ \(Type1 _ ty_f_m_b, _) ->
 118         check_type1_eq ex ast ty_ma ty_f_mb $ \Refl ->
 119         check_type1_constraint ex (Proxy::Proxy Monad) ast ty_ma $ \Dict ->
 120         k (Type_Root $ ty_m $ Type1 m ty_f_m_b) $ Forall_Repr_with_Context $
 121          \c -> (>>=) (ma c) (f c)