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.Monoid
  19 import Data.Proxy (Proxy(..))
  20 import Data.Type.Equality ((:~:)(Refl))
  21 import Prelude hiding ((<$>), Monad(..))
  22
  23 import Language.Symantic.Type
  24 import Language.Symantic.Repr
  25 import Language.Symantic.Expr.Root
  26 import Language.Symantic.Expr.Error
  27 import Language.Symantic.Expr.From
  28 import Language.Symantic.Expr.Lambda
  29 import Language.Symantic.Expr.Functor
  30 import Language.Symantic.Trans.Common
  31
  32 -- * Class 'Sym_Monad'
  33 -- | Symantic.
  34 class Sym_Functor repr => Sym_Monad repr where
  35         return :: Monad m => repr a -> repr (m a)
  36         (>>=)  :: Monad m => repr (m a) -> repr (a -> m b) -> repr (m b)
  37
  38         default return :: (Trans t repr, Monad m)
  39          => t repr a -> t repr (m a)
  40         default (>>=) :: (Trans t repr, Monad m)
  41          => t repr (m a) -> t repr (a -> m b) -> t repr (m b)
  42
  43         return = trans_map1 return
  44         (>>=)  = trans_map2 (>>=)
  45 infixl 1 >>=
  46 instance Sym_Monad Repr_Host where
  47         return = Monad.liftM Monad.return
  48         (>>=)  = Monad.liftM2 (Monad.>>=)
  49 instance Sym_Monad Repr_Text where
  50         return = repr_text_app1 "return"
  51         (>>=) (Repr_Text g) (Repr_Text ma) =
  52                 Repr_Text $ \p v ->
  53                         let p' = precedence_Bind in
  54                         paren p p' $ g p' v <> " >>= " <> ma p' v
  55 instance
  56  ( Sym_Monad r1
  57  , Sym_Monad r2
  58  ) => Sym_Monad (Dup r1 r2) where
  59         return (a1 `Dup` a2) =
  60                 return a1 `Dup` return a2
  61         (>>=) (m1 `Dup` m2) (f1 `Dup` f2) =
  62                 (>>=) m1 f1 `Dup` (>>=) m2 f2
  63
  64 -- * Type 'Expr_Monad'
  65 -- | Expression.
  66 data Expr_Monad (root:: *)
  67 type instance Root_of_Expr      (Expr_Monad root)      = root
  68 type instance Type_of_Expr      (Expr_Monad root)      = No_Type
  69 type instance Sym_of_Expr       (Expr_Monad root) repr = (Sym_Monad repr)
  70 type instance Error_of_Expr ast (Expr_Monad root)      = No_Error_Expr
  71
  72 return_from
  73  :: forall root ty ast hs ret.
  74  ( ty ~ Type_Root_of_Expr (Expr_Monad root)
  75  , Eq_Type ty
  76  , Type1_from ast ty
  77  , Expr_from ast root
  78  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  79                    (Error_of_Expr ast root)
  80  , Root_of_Expr root ~ root
  81  , Constraint_Type1 Monad ty
  82  ) => ast -> ast
  83  -> Expr_From ast (Expr_Monad root) hs ret
  84 return_from ast_f ast_a ex ast ctx k =
  85  -- return :: Monad f => a -> f a
  86         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) Fun.id $
  87         type1_from (Proxy::Proxy ty) ast_f $ \_f ty_f -> Right $
  88                 expr_from (Proxy::Proxy root) ast_a ctx $
  89                  \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
  90                 let ty_fa = ty_f ty_a in
  91                 check_constraint_type1 ex (Proxy::Proxy Monad) ast ty_fa $ \Dict ->
  92                 k ty_fa $ Forall_Repr_with_Context $
  93                  \c -> return (a c)
  94
  95 bind_from
  96  :: forall root ty ast hs ret.
  97  ( ty ~ Type_Root_of_Expr (Expr_Monad root)
  98  , Eq_Type ty
  99  , Eq_Type1 ty
 100  , Expr_from ast root
 101  , Lift_Type   Type_Fun (Type_of_Expr root)
 102  , Unlift_Type Type_Fun (Type_of_Expr root)
 103  , Unlift_Type1 (Type_of_Expr root)
 104  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 105                    (Error_of_Expr ast root)
 106  , Root_of_Expr root ~ root
 107  , Constraint_Type1 Monad ty
 108  ) => ast -> ast
 109  -> Expr_From ast (Expr_Monad root) hs ret
 110 bind_from ast_ma ast_f ex ast ctx k =
 111  -- (>>=) :: Monad m => m a -> (a -> m b) -> m b
 112         expr_from (Proxy::Proxy root) ast_ma ctx $
 113          \(ty_ma::ty h_ma) (Forall_Repr_with_Context ma) ->
 114         expr_from (Proxy::Proxy root) ast_f ctx $
 115          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 116         check_type1 ex ast ty_ma $ \(Type_Type1 m ty_m_a, Lift_Type1 ty_m) ->
 117         check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_mb
 118          :: Type_Fun ty h_f) ->
 119         check_eq_type ex ast ty_m_a ty_f_a $ \Refl ->
 120         check_type1 ex ast ty_f_mb $ \(Type_Type1 _ ty_f_m_b, _) ->
 121         check_eq_type1 ex ast ty_ma ty_f_mb $ \Refl ->
 122         check_constraint_type1 ex (Proxy::Proxy Monad) ast ty_ma $ \Dict ->
 123         k (Type_Root $ ty_m $ Type_Type1 m ty_f_m_b) $ Forall_Repr_with_Context $
 124          \c -> (>>=) (ma c) (f c)