Language/Symantic/Expr/Applicative.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE ScopedTypeVariables #-}
   7 {-# LANGUAGE TypeFamilies #-}
   8 {-# LANGUAGE TypeOperators #-}
   9 -- | Expression for 'Applicative'.
  10 module Language.Symantic.Expr.Applicative where
  11
  12 import Control.Applicative (Applicative)
  13 import Data.Proxy (Proxy(..))
  14 import Data.Type.Equality ((:~:)(Refl))
  15 import Prelude hiding (Applicative(..))
  16
  17 import Language.Symantic.Type
  18 -- import Language.Symantic.Repr.Dup
  19 import Language.Symantic.Trans.Common
  20 import Language.Symantic.Expr.Common
  21 import Language.Symantic.Expr.Lambda
  22 import Language.Symantic.Expr.Functor
  23
  24 class Sym_Applicative repr where
  25         pure  :: Applicative f => repr a -> repr (f a)
  26         -- (*>)  :: Applicative f => repr (f a) -> repr (f b) -> repr (f b)
  27         -- (<*)  :: Applicative f => repr (f a) -> repr (f b) -> repr (f a)
  28
  29         default pure :: (Trans t repr, Applicative f) => t repr a -> t repr (f a)
  30         pure = trans_map1 pure
  31
  32 class Sym_Functor lam repr => Sym_Applicative_Lam lam repr where
  33         (<*>) :: Applicative f => repr (f (Lambda lam a b)) -> repr (f a) -> repr (f b)
  34         -- (*>)  :: Applicative f => repr (f a) -> repr (f b) -> repr (f b)
  35         -- (<*)  :: Applicative f => repr (f a) -> repr (f b) -> repr (f a)
  36
  37         default (<*>) :: (Trans t repr, Applicative f) => t repr (f (Lambda lam a b)) -> t repr (f a) -> t repr (f b)
  38         -- default (*>)  :: (Trans t, Applicative f) => t repr (f a) -> t repr (f b) -> t repr (f b)
  39         -- default (<*)  :: (Trans t, Applicative f) => t repr (f a) -> t repr (f b) -> t repr (f a)
  40         (<*>) = trans_map2 (<*>)
  41
  42 -- * Type 'Expr_Applicative'
  43 -- | Expression.
  44 data Expr_Applicative (lam:: * -> *) (root:: *)
  45 type instance Root_of_Expr      (Expr_Applicative lam root)      = root
  46 type instance Type_of_Expr      (Expr_Applicative lam root)      = No_Type
  47 type instance Sym_of_Expr       (Expr_Applicative lam root) repr = (Sym_Applicative repr, Sym_Applicative_Lam lam repr)
  48 type instance Error_of_Expr ast (Expr_Applicative lam root)      = No_Error_Expr
  49
  50 -- * Class 'Type1_from'
  51 -- | Parse given @ast@ into a 'Root_of_Type',
  52 -- or return an 'Error_of_Type'.
  53 class Type1_from ast (ty:: * -> *) where
  54         type1_from
  55          :: Proxy ty
  56          -> ast
  57          -> (forall h. (Root_of_Type ty h -> Root_of_Type ty h)
  58                     -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
  59          ->            Either (Error_of_Type ast (Root_of_Type ty)) ret
  60
  61 pure_from
  62  :: forall root ty lam ast hs ret.
  63  ( ty ~ Type_Root_of_Expr (Expr_Applicative lam root)
  64  , Eq_Type (Type_Root_of_Expr root)
  65  , Type1_from ast (Type_of_Expr root)
  66  , Expr_from ast root
  67  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  68                    (Error_of_Expr ast root)
  69  , Root_of_Expr root ~ root
  70  , Constraint1_Type Functor_with_Lambda ty
  71  , Constraint1_Type Applicative ty
  72  ) => ast -> ast
  73  -> Expr_From ast (Expr_Applicative lam root) hs ret
  74 pure_from ast_f ast_a ex ast ctx k =
  75  -- pure :: Applicative f => a -> f a
  76         case type1_from (Proxy::Proxy ty_root)
  77          ast_f (Right . Exists_Type1) of
  78          Left err -> Left $ error_expr ex $ Error_Expr_Type err ast
  79          Right (Exists_Type1 ty_f) ->
  80                 expr_from (Proxy::Proxy root) ast_a ctx $
  81                  \(ty_a::Type_Root_of_Expr root h_a) (Forall_Repr_with_Context a) ->
  82                 let ty_fa = (Type_Root $ ty_f $ Type_Type1 f ty_a) in
  83                 check_constraint1_type ex (Proxy::Proxy Applicative) ast ty_fa $ \Dict ->
  84                 k ty_fa $ Forall_Repr_with_Context $
  85                  \c -> pure (a c)
  86
  87 ltstargt_from
  88  :: forall root ty lam ast hs ret.
  89  ( ty ~ Type_Root_of_Expr (Expr_Applicative lam root)
  90  , Eq_Type (Type_Root_of_Expr root)
  91  , Expr_from ast root
  92  , Type_Lift   (Type_Fun lam) (Type_of_Expr root)
  93  , Type_Unlift (Type_Fun lam) (Type_of_Expr root)
  94  , Type_Unlift1 (Type_of_Expr root)
  95  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  96                    (Error_of_Expr ast root)
  97  , Root_of_Expr root ~ root
  98  , Constraint1_Type Applicative ty
  99  ) => ast -> ast
 100  -> Expr_From ast (Expr_Applicative lam root) hs ret
 101 ltstargt_from ast_g ast_fa ex ast ctx k =
 102  -- (<*>) :: Applicative f => f (a -> b) -> f a -> f b
 103         expr_from (Proxy::Proxy root) ast_g ctx $
 104          \(ty_fg::Type_Root_of_Expr root h_fg) (Forall_Repr_with_Context fg) ->
 105         expr_from (Proxy::Proxy root) ast_fa ctx $
 106          \(ty_fa::Type_Root_of_Expr root h_fa) (Forall_Repr_with_Context fa) ->
 107         check_type1 ex ast ty_fg $ \(Type_Type1 _f (ty_g::Type_Root_of_Expr root h_g), _) ->
 108         check_type_fun ex ast ty_g $ \(ty_g_a `Type_Fun` ty_g_b
 109          :: Type_Fun lam (Type_Root_of_Expr root) h_g) ->
 110         check_type1 ex ast ty_fa $ \(Type_Type1 f ty_fa_a, Type_Lift1 ty_f) ->
 111         check_constraint1_type ex (Proxy::Proxy Applicative) ast ty_fa $ \Dict ->
 112         check_eq_type ex ast ty_g_a ty_fa_a $ \Refl ->
 113         k (Type_Root $ ty_f $ Type_Type1 f ty_g_b) $ Forall_Repr_with_Context $
 114          \c -> (<*>) (fg c) (fa c)