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