Language/Symantic/Expr/Monoid.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 'Monoid'.
  12 module Language.Symantic.Expr.Monoid where
  13
  14 import Data.Monoid (Monoid)
  15 import Data.Proxy (Proxy(..))
  16 import Data.Type.Equality ((:~:)(Refl))
  17 import Prelude hiding ((<$>), Monoid(..))
  18
  19 import Language.Symantic.Type
  20 import Language.Symantic.Trans.Common
  21 import Language.Symantic.Expr.Root
  22 import Language.Symantic.Expr.Error
  23 import Language.Symantic.Expr.From
  24 -- import Language.Symantic.Expr.Lambda
  25 -- import Language.Symantic.Expr.Functor
  26
  27 -- * Class 'Sym_Monoid'
  28 -- | Symantic.
  29 class Sym_Monoid repr where
  30         mempty  :: Monoid a => repr a
  31         mappend :: Monoid a => repr a -> repr a -> repr a
  32         default mempty  :: (Trans t repr, Monoid a) => t repr a
  33         default mappend :: (Trans t repr, Monoid a) => t repr a -> t repr a -> t repr a
  34         mempty  = trans_lift mempty
  35         mappend = trans_map2 mappend
  36
  37 -- | 'mappend' alias.
  38 (<>) ::
  39  ( Sym_Monoid repr
  40  , Monoid a )
  41  => repr a -> repr a -> repr a
  42 (<>) = mappend
  43 infixr 6 <>
  44
  45 -- * Type 'Expr_Monoid'
  46 -- | Expression.
  47 data Expr_Monoid (lam:: * -> *) (root:: *)
  48 type instance Root_of_Expr      (Expr_Monoid lam root)      = root
  49 type instance Type_of_Expr      (Expr_Monoid lam root)      = No_Type
  50 type instance Sym_of_Expr       (Expr_Monoid lam root) repr = (Sym_Monoid repr)
  51 type instance Error_of_Expr ast (Expr_Monoid lam root)      = No_Error_Expr
  52
  53 instance Constraint_Type Monoid (Type_Var0 root)
  54 instance Constraint_Type Monoid (Type_Var1 root)
  55
  56 -- | Parse 'mempty'.
  57 mempty_from
  58  :: forall root ty lam ast hs ret.
  59  ( ty ~ Type_Root_of_Expr (Expr_Monoid lam root)
  60  , Type_from ast ty
  61  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  62                    (Error_of_Expr ast root)
  63  , Root_of_Expr root ~ root
  64  , Constraint_Type Monoid ty
  65  ) => ast
  66  -> Expr_From ast (Expr_Monoid lam root) hs ret
  67 mempty_from ast_a ex ast _ctx k =
  68  -- mempty :: Monoid a => a
  69         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $
  70         type_from (Proxy::Proxy ty) ast_a $ \ty_a -> Right $
  71         check_constraint_type ex (Proxy::Proxy Monoid) ast ty_a $ \Dict ->
  72         k ty_a $ Forall_Repr_with_Context $
  73         const mempty
  74
  75 -- | Parse 'mappend'.
  76 mappend_from
  77  :: forall root ty lam ast hs ret.
  78  ( ty ~ Type_Root_of_Expr (Expr_Monoid lam root)
  79  , Eq_Type ty
  80  , Expr_from ast root
  81  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  82                    (Error_of_Expr ast root)
  83  , Root_of_Expr root ~ root
  84  , Constraint_Type Monoid ty
  85  ) => ast -> ast
  86  -> Expr_From ast (Expr_Monoid lam root) hs ret
  87 mappend_from ast_x ast_y ex ast ctx k =
  88  -- mappend :: Monoid a => a -> a -> a
  89         expr_from (Proxy::Proxy root) ast_x ctx $
  90          \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
  91         expr_from (Proxy::Proxy root) ast_y ctx $
  92          \(ty_y::ty h_y) (Forall_Repr_with_Context y) ->
  93         check_eq_type ex ast ty_x ty_y $ \Refl ->
  94         check_constraint_type ex (Proxy::Proxy Monoid) ast ty_x $ \Dict ->
  95         k ty_x $ Forall_Repr_with_Context $
  96          \c -> mappend (x c) (y c)