Language/Symantic/Expr/Applicative.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 'Applicative'.
  12 module Language.Symantic.Expr.Applicative where
  13
  14 import Control.Applicative (Applicative)
  15 import Data.Proxy (Proxy(..))
  16 import Data.Type.Equality ((:~:)(Refl))
  17 import Prelude hiding (Functor(..), (<$>), Applicative(..), id, const)
  18 import qualified Data.Function as Fun
  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_Applicative'
  29 -- | Symantic.
  30 class Sym_Functor repr => Sym_Applicative repr where
  31         pure  :: Applicative f => repr a -> repr (f a)
  32         (<*>) :: Applicative f => repr (f ((->) a b)) -> repr (f a) -> repr (f b)
  33         default pure  :: (Trans t repr, Applicative f) => t repr a -> t repr (f a)
  34         default (<*>) :: (Trans t repr, Applicative f)
  35          => t repr (f ((->) a b)) -> t repr (f a) -> t repr (f b)
  36         pure = trans_map1 pure
  37         (<*>) = trans_map2 (<*>)
  38         (*>) :: Applicative f => repr (f a) -> repr (f b) -> repr (f b)
  39         (<*) :: Applicative f => repr (f a) -> repr (f b) -> repr (f a)
  40         x *> y = (lam Fun.id <$ x) <*> y
  41         x <* y = (lam (lam . Fun.const) <$> x) <*> y
  42 infixl 4  *>
  43 infixl 4 <*
  44 infixl 4 <*>
  45
  46 -- * Type 'Expr_Applicative'
  47 -- | Expression.
  48 data Expr_Applicative (root:: *)
  49 type instance Root_of_Expr      (Expr_Applicative root)      = root
  50 type instance Type_of_Expr      (Expr_Applicative root)      = No_Type
  51 type instance Sym_of_Expr       (Expr_Applicative root) repr = (Sym_Applicative repr)
  52 type instance Error_of_Expr ast (Expr_Applicative root)      = No_Error_Expr
  53 instance Constraint_Type1 Applicative (Type_Type0 px root)
  54 instance Constraint_Type1 Applicative (Type_Var1 root)
  55 -- instance Constraint_Type1 Applicative (Type_Type2 px root)
  56
  57 -- | Parse 'pure'.
  58 pure_from
  59  :: forall root ty ast hs ret.
  60  ( ty ~ Type_Root_of_Expr (Expr_Applicative root)
  61  , Eq_Type ty
  62  , Type1_from ast ty
  63  , Expr_from ast root
  64  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  65                    (Error_of_Expr ast root)
  66  , Root_of_Expr root ~ root
  67  , Constraint_Type1 Applicative ty
  68  ) => ast -> ast
  69  -> Expr_From ast (Expr_Applicative root) hs ret
  70 pure_from ast_f ast_a ex ast ctx k =
  71  -- pure :: Applicative f => a -> f a
  72         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) Fun.id $
  73         type1_from (Proxy::Proxy ty) ast_f $ \_f ty_f -> Right $
  74                 expr_from (Proxy::Proxy root) ast_a ctx $
  75                  \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
  76                 let ty_fa = ty_f ty_a in
  77                 check_constraint_type1 ex (Proxy::Proxy Applicative) ast ty_fa $ \Dict ->
  78                 k ty_fa $ Forall_Repr_with_Context $
  79                  \c -> pure (a c)
  80
  81 -- | Parse '<*>'.
  82 ltstargt_from
  83  :: forall root ty ast hs ret.
  84  ( ty ~ Type_Root_of_Expr (Expr_Applicative root)
  85  , Eq_Type  ty
  86  , Eq_Type1 ty
  87  , Expr_from ast root
  88  , Lift_Type   Type_Fun (Type_of_Expr root)
  89  , Unlift_Type Type_Fun (Type_of_Expr root)
  90  , Unlift_Type1 (Type_of_Expr root)
  91  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  92                    (Error_of_Expr ast root)
  93  , Root_of_Expr root ~ root
  94  , Constraint_Type1 Applicative ty
  95  ) => ast -> ast
  96  -> Expr_From ast (Expr_Applicative root) hs ret
  97 ltstargt_from ast_fg ast_fa ex ast ctx k =
  98  -- (<*>) :: Applicative f => f (a -> b) -> f a -> f b
  99         expr_from (Proxy::Proxy root) ast_fg ctx $
 100          \(ty_fg::ty h_fg) (Forall_Repr_with_Context fg) ->
 101         expr_from (Proxy::Proxy root) ast_fa ctx $
 102          \(ty_fa::ty h_fa) (Forall_Repr_with_Context fa) ->
 103         check_type1 ex ast ty_fg $ \(Type_Type1 _f (ty_g::ty h_g), _) ->
 104         check_type1 ex ast ty_fa $ \(Type_Type1 f ty_fa_a, Lift_Type1 ty_f) ->
 105         check_eq_type1 ex ast ty_fg ty_fa $ \Refl ->
 106         check_type_fun ex ast ty_g $ \(Type_Type2 Proxy ty_g_a ty_g_b
 107          :: Type_Fun ty h_g) ->
 108         check_constraint_type1 ex (Proxy::Proxy Applicative) ast ty_fa $ \Dict ->
 109         check_eq_type ex ast ty_g_a ty_fa_a $ \Refl ->
 110         k (Type_Root $ ty_f $ Type_Type1 f ty_g_b) $ Forall_Repr_with_Context $
 111          \c -> (<*>) (fg c) (fa c)