1 {-# LANGUAGE DefaultSignatures #-}
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
15 import Control.Applicative (Applicative)
16 import qualified Control.Applicative as Applicative
18 import qualified Data.Function as Fun
20 import Data.Proxy (Proxy(..))
21 import Data.Type.Equality ((:~:)(Refl))
22 import Prelude hiding (Functor(..), (<$>), Applicative(..), id, const)
24 import Language.Symantic.Type
25 import Language.Symantic.Repr
26 import Language.Symantic.Trans.Common
27 import Language.Symantic.Expr.Root
28 import Language.Symantic.Expr.Error
29 import Language.Symantic.Expr.From
30 import Language.Symantic.Expr.Lambda
31 import Language.Symantic.Expr.Functor
33 -- * Class 'Sym_Applicative'
35 class Sym_Functor repr => Sym_Applicative repr where
36 pure :: Applicative f => repr a -> repr (f a)
37 (<*>) :: Applicative f => repr (f ((->) a b)) -> repr (f a) -> repr (f b)
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 pure = trans_map1 pure
42 (<*>) = trans_map2 (<*>)
43 (*>) :: Applicative f => repr (f a) -> repr (f b) -> repr (f b)
44 (<*) :: Applicative f => repr (f a) -> repr (f b) -> repr (f a)
45 x *> y = (lam Fun.id <$ x) <*> y
46 x <* y = (lam (lam . Fun.const) <$> x) <*> y
50 instance Sym_Applicative Repr_Host where
51 pure = liftM Applicative.pure
52 (<*>) = liftM2 (Applicative.<*>)
53 instance Sym_Applicative Repr_Text where
54 pure = repr_text_app1 "pure"
55 (<*>) (Repr_Text fg) (Repr_Text fa) =
57 let p' = precedence_LtStarGt in
58 paren p p' $ fg p' v <> " <*> " <> fa p' v
62 ) => Sym_Applicative (Dup r1 r2) where
65 (<*>) (f1 `Dup` f2) (m1 `Dup` m2) =
66 (<*>) f1 m1 `Dup` (<*>) f2 m2
68 -- * Type 'Expr_Applicative'
70 data Expr_Applicative (root:: *)
71 type instance Root_of_Expr (Expr_Applicative root) = root
72 type instance Type_of_Expr (Expr_Applicative root) = No_Type
73 type instance Sym_of_Expr (Expr_Applicative root) repr = (Sym_Applicative repr)
74 type instance Error_of_Expr ast (Expr_Applicative root) = No_Error_Expr
78 :: forall root ty ast hs ret.
79 ( ty ~ Type_Root_of_Expr (Expr_Applicative root)
83 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
84 (Error_of_Expr ast root)
85 , Root_of_Expr root ~ root
86 , Type1_Constraint Applicative ty
88 -> ExprFrom ast (Expr_Applicative root) hs ret
89 pure_from ast_f ast_a ex ast ctx k =
90 -- pure :: Applicative f => a -> f a
91 either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) Fun.id $
92 type1_from (Proxy::Proxy ty) ast_f $ \_f ty_f -> Right $
93 expr_from (Proxy::Proxy root) ast_a ctx $
94 \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
95 let ty_fa = ty_f ty_a in
96 check_type1_constraint ex (Proxy::Proxy Applicative) ast ty_fa $ \Dict ->
97 k ty_fa $ Forall_Repr_with_Context $
102 :: forall root ty ast hs ret.
103 ( ty ~ Type_Root_of_Expr (Expr_Applicative root)
107 , Type0_Lift Type_Fun (Type_of_Expr root)
108 , Type0_Unlift Type_Fun (Type_of_Expr root)
109 , Type1_Unlift (Type_of_Expr root)
110 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
111 (Error_of_Expr ast root)
112 , Root_of_Expr root ~ root
113 , Type1_Constraint Applicative ty
115 -> ExprFrom ast (Expr_Applicative root) hs ret
116 ltstargt_from ast_fg ast_fa ex ast ctx k =
117 -- (<*>) :: Applicative f => f (a -> b) -> f a -> f b
118 expr_from (Proxy::Proxy root) ast_fg ctx $
119 \(ty_fg::ty h_fg) (Forall_Repr_with_Context fg) ->
120 expr_from (Proxy::Proxy root) ast_fa ctx $
121 \(ty_fa::ty h_fa) (Forall_Repr_with_Context fa) ->
122 check_type1 ex ast ty_fg $ \(Type1 _f (ty_g::ty h_g), _) ->
123 check_type1 ex ast ty_fa $ \(Type1 f ty_fa_a, Type1_Lift ty_f) ->
124 check_type1_eq ex ast ty_fg ty_fa $ \Refl ->
125 check_type_fun ex ast ty_g $ \(Type2 Proxy ty_g_a ty_g_b
126 :: Type_Fun ty h_g) ->
127 check_type1_constraint ex (Proxy::Proxy Applicative) ast ty_fa $ \Dict ->
128 check_type0_eq ex ast ty_g_a ty_fa_a $ \Refl ->
129 k (Type_Root $ ty_f $ Type1 f ty_g_b) $ Forall_Repr_with_Context $
130 \c -> (<*>) (fg c) (fa c)