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 {-# LANGUAGE UndecidableInstances #-}
  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 (Applicative(..))
  18
  19 import Language.Symantic.Type
  20 import Language.Symantic.Trans.Common
  21 import Language.Symantic.Expr.Common
  22 import Language.Symantic.Expr.Lambda
  23 import Language.Symantic.Expr.Functor
  24
  25 -- * Class 'Sym_Applicative'
  26 -- | Symantic.
  27 class Sym_Applicative repr where
  28         pure  :: Applicative f => repr a -> repr (f a)
  29         -- (*>)  :: Applicative f => repr (f a) -> repr (f b) -> repr (f b)
  30         -- (<*)  :: Applicative f => repr (f a) -> repr (f b) -> repr (f a)
  31
  32         default pure :: (Trans t repr, Applicative f) => t repr a -> t repr (f a)
  33         pure = trans_map1 pure
  34
  35 -- * Class 'Sym_Applicative_Lam'
  36 -- | Symantic requiring a 'Lambda'.
  37 class Sym_Functor lam repr => Sym_Applicative_Lam lam repr where
  38         (<*>) :: Applicative_with_Lambda f => repr (f (Lambda lam a b)) -> repr (f a) -> repr (f b)
  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
  42         default (<*>) :: (Trans t repr, Applicative_with_Lambda f) => t repr (f (Lambda lam a b)) -> t repr (f a) -> t repr (f b)
  43         -- default (*>)  :: (Trans t, Applicative f) => t repr (f a) -> t repr (f b) -> t repr (f b)
  44         -- default (<*)  :: (Trans t, Applicative f) => t repr (f a) -> t repr (f b) -> t repr (f a)
  45         (<*>) = trans_map2 (<*>)
  46 infixl 4 <*>
  47
  48 -- ** Class 'Applicative_with_Lambda'
  49 -- | A class alias to join 'Traversable' to 'Applicative'.
  50 --
  51 -- NOTE: see comment of 'Functor_with_Lambda'.
  52 class    (Applicative f, Traversable f) => Applicative_with_Lambda f
  53 instance (Applicative f, Traversable f) => Applicative_with_Lambda f
  54 instance Constraint_Type1 Applicative_with_Lambda (Type_Type1 t1 root)
  55 instance Constraint_Type1 Applicative_with_Lambda (Type_Type2 c2 t2 root)
  56 instance Constraint_Type1 Applicative_with_Lambda (Type_Var root)
  57
  58 -- * Type 'Expr_Applicative'
  59 -- | Expression.
  60 data Expr_Applicative (lam:: * -> *) (root:: *)
  61 type instance Root_of_Expr      (Expr_Applicative lam root)      = root
  62 type instance Type_of_Expr      (Expr_Applicative lam root)      = No_Type
  63 type instance Sym_of_Expr       (Expr_Applicative lam root) repr = (Sym_Applicative repr, Sym_Applicative_Lam lam repr)
  64 type instance Error_of_Expr ast (Expr_Applicative lam root)      = No_Error_Expr
  65
  66 pure_from
  67  :: forall root ty ty_root lam ast hs ret.
  68  ( ty ~ Type_Root_of_Expr (Expr_Applicative lam root)
  69  , ty_root ~ Type_Root_of_Expr root
  70  , Eq_Type (Type_Root_of_Expr root)
  71  , Type1_from ast (Type_Root_of_Expr root)
  72  , Expr_from ast root
  73  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  74                    (Error_of_Expr ast root)
  75  , Root_of_Expr root ~ root
  76  , Constraint_Type1 Applicative_with_Lambda ty
  77  ) => ast -> ast
  78  -> Expr_From ast (Expr_Applicative lam root) hs ret
  79 pure_from ast_f ast_a ex ast ctx k =
  80  -- pure :: Applicative f => a -> f a
  81         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $
  82         type1_from (Proxy::Proxy ty_root) ast_f $ \_f ty_f -> Right $
  83                 expr_from (Proxy::Proxy root) ast_a ctx $
  84                  \(ty_a::Type_Root_of_Expr root h_a) (Forall_Repr_with_Context a) ->
  85                 let ty_fa = ty_f ty_a in
  86                 check_constraint1_type ex (Proxy::Proxy Applicative_with_Lambda) ast ty_fa $ \Dict ->
  87                 k ty_fa $ Forall_Repr_with_Context $
  88                  \c -> pure (a c)
  89
  90 ltstargt_from
  91  :: forall root ty lam ast hs ret.
  92  ( ty ~ Type_Root_of_Expr (Expr_Applicative lam root)
  93  , String_from_Type ty
  94  , Eq_Type (Type_Root_of_Expr root)
  95  , Eq_Type1 (Type_Root_of_Expr root)
  96  , Expr_from ast root
  97  , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
  98  , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
  99  , Unlift_Type1 (Type_of_Expr root)
 100  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 101                    (Error_of_Expr ast root)
 102  , Root_of_Expr root ~ root
 103  , Constraint_Type1 Applicative_with_Lambda ty
 104  ) => ast -> ast
 105  -> Expr_From ast (Expr_Applicative lam root) hs ret
 106 ltstargt_from ast_fg ast_fa ex ast ctx k =
 107  -- (<*>) :: Applicative f => f (a -> b) -> f a -> f b
 108         expr_from (Proxy::Proxy root) ast_fg ctx $
 109          \(ty_fg::Type_Root_of_Expr root h_fg) (Forall_Repr_with_Context fg) ->
 110         expr_from (Proxy::Proxy root) ast_fa ctx $
 111          \(ty_fa::Type_Root_of_Expr root h_fa) (Forall_Repr_with_Context fa) ->
 112         check_type1 ex ast ty_fg $ \(Type_Type1 _f (ty_g::Type_Root_of_Expr root h_g), _) ->
 113         check_type1 ex ast ty_fa $ \(Type_Type1 f ty_fa_a, Lift_Type1 ty_f) ->
 114         check_eq_type1 ex ast ty_fg ty_fa $ \Refl ->
 115         check_type_fun ex ast ty_g $ \(ty_g_a `Type_Fun` ty_g_b
 116          :: Type_Fun lam (Type_Root_of_Expr root) h_g) ->
 117         check_constraint1_type ex (Proxy::Proxy Applicative_with_Lambda) ast ty_fa $ \Dict ->
 118         check_eq_type ex ast ty_g_a ty_fa_a $ \Refl ->
 119         k (Type_Root $ ty_f $ Type_Type1 f ty_g_b) $ Forall_Repr_with_Context $
 120          \c -> (<*>) (fg c) (fa c)