Language/Symantic/Expr/Applicative.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 'Applicative'.
  13 module Language.Symantic.Expr.Applicative where
  14
  15 import Control.Applicative (Applicative)
  16 import qualified Control.Applicative as Applicative
  17 import Control.Monad
  18 import qualified Data.Function as Fun
  19 import Data.Proxy (Proxy(..))
  20 import Data.Type.Equality ((:~:)(Refl))
  21 import Prelude hiding (Functor(..), (<$>), Applicative(..), id, const)
  22
  23 import Language.Symantic.Type
  24 import Language.Symantic.Repr
  25 import Language.Symantic.Trans.Common
  26 import Language.Symantic.Expr.Root
  27 import Language.Symantic.Expr.Error
  28 import Language.Symantic.Expr.From
  29 import Language.Symantic.Expr.Lambda
  30 import Language.Symantic.Expr.Functor
  31
  32 -- * Class 'Sym_Applicative'
  33 -- | Symantic.
  34 class Sym_Functor repr => Sym_Applicative repr where
  35         pure  :: Applicative f => repr a -> repr (f a)
  36         (<*>) :: Applicative f => repr (f ((->) a b)) -> repr (f a) -> repr (f b)
  37
  38         default pure  :: (Trans t repr, Applicative f) => t repr a -> t repr (f a)
  39         default (<*>) :: (Trans t repr, Applicative f)
  40          => t repr (f ((->) a b)) -> t repr (f a) -> t repr (f b)
  41
  42         pure = trans_map1 pure
  43         (<*>) = trans_map2 (<*>)
  44         (*>) :: Applicative f => repr (f a) -> repr (f b) -> repr (f b)
  45         (<*) :: Applicative f => repr (f a) -> repr (f b) -> repr (f a)
  46         x *> y = (lam Fun.id <$ x) <*> y
  47         x <* y = (lam (lam . Fun.const) <$> x) <*> y
  48
  49 infixl 4  *>
  50 infixl 4 <*
  51 infixl 4 <*>
  52
  53 instance Sym_Applicative Repr_Host where
  54         pure  = liftM Applicative.pure
  55         (<*>) = liftM2 (Applicative.<*>)
  56 instance Sym_Applicative Repr_Text where
  57         pure  = repr_text_app1 "pure"
  58         (<*>) = repr_text_infix "<*>" (Precedence 4)
  59         (<* ) = repr_text_infix "<*"  (Precedence 4)
  60         ( *>) = repr_text_infix "*>"  (Precedence 4)
  61 instance (Sym_Applicative r1, Sym_Applicative r2) => Sym_Applicative (Repr_Dup r1 r2) where
  62         pure (a1 `Repr_Dup` a2) =
  63                 pure a1 `Repr_Dup` pure a2
  64         (<*>) (f1 `Repr_Dup` f2) (m1 `Repr_Dup` m2) =
  65                 (<*>) f1 m1 `Repr_Dup` (<*>) f2 m2
  66
  67 -- * Type 'Expr_Applicative'
  68 -- | Expression.
  69 data Expr_Applicative (root:: *)
  70 type instance Root_of_Expr      (Expr_Applicative root)      = root
  71 type instance Type_of_Expr      (Expr_Applicative root)      = No_Type
  72 type instance Sym_of_Expr       (Expr_Applicative root) repr = (Sym_Applicative repr)
  73 type instance Error_of_Expr ast (Expr_Applicative root)      = No_Error_Expr
  74
  75 -- | Parse 'pure'.
  76 pure_from
  77  :: forall root ty ast hs ret.
  78  ( ty ~ Type_Root_of_Expr (Expr_Applicative root)
  79  , Type0_Eq ty
  80  , Type1_From ast ty
  81  , Expr_From ast root
  82  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  83                    (Error_of_Expr ast root)
  84  , Root_of_Expr root ~ root
  85  , Type1_Constraint Applicative ty
  86  ) => ast -> ast
  87  -> ExprFrom ast (Expr_Applicative root) hs ret
  88 pure_from ast_f ast_a ex ast ctx k =
  89  -- pure :: Applicative f => a -> f a
  90         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) Fun.id $
  91         type1_from (Proxy::Proxy ty) ast_f $ \_f ty_f -> Right $
  92                 expr_from (Proxy::Proxy root) ast_a ctx $
  93                  \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
  94                 let ty_fa = ty_f ty_a in
  95                 check_type1_constraint ex (Proxy::Proxy Applicative) ast ty_fa $ \Dict ->
  96                 k ty_fa $ Forall_Repr_with_Context $
  97                  \c -> pure (a c)
  98
  99 -- | Parse '<*>'.
 100 ltstargt_from
 101  :: forall root ty ast hs ret.
 102  ( ty ~ Type_Root_of_Expr (Expr_Applicative root)
 103  , Expr_From ast root
 104  , Type0_Eq ty
 105  , Type1_Eq ty
 106  , Type0_Lift   Type_Fun (Type_of_Expr root)
 107  , Type0_Unlift Type_Fun (Type_of_Expr root)
 108  , Type1_Unlift (Type_of_Expr root)
 109  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 110                    (Error_of_Expr ast root)
 111  , Root_of_Expr root ~ root
 112  , Type1_Constraint Applicative ty
 113  ) => ast -> ast
 114  -> ExprFrom ast (Expr_Applicative root) hs ret
 115 ltstargt_from ast_fg ast_fa ex ast ctx k =
 116  -- (<*>) :: Applicative f => f (a -> b) -> f a -> f b
 117         expr_from (Proxy::Proxy root) ast_fg ctx $
 118          \(ty_fg::ty h_fg) (Forall_Repr_with_Context fg) ->
 119         expr_from (Proxy::Proxy root) ast_fa ctx $
 120          \(ty_fa::ty h_fa) (Forall_Repr_with_Context fa) ->
 121         check_type1 ex ast ty_fg $ \(Type1 _f (ty_g::ty h_g), _) ->
 122         check_type1 ex ast ty_fa $ \(Type1 f ty_fa_a, Type1_Lift ty_f) ->
 123         check_type1_eq ex ast ty_fg ty_fa $ \Refl ->
 124         check_type_fun ex ast ty_g $ \(Type2 Proxy ty_g_a ty_g_b) ->
 125         check_type1_constraint ex (Proxy::Proxy Applicative) ast ty_fa $ \Dict ->
 126         check_type0_eq ex ast ty_g_a ty_fa_a $ \Refl ->
 127         k (Type_Root $ ty_f $ Type1 f ty_g_b) $ Forall_Repr_with_Context $
 128          \c -> (<*>) (fg c) (fa c)