symantic-lib/Language/Symantic/Lib/Applicative.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Applicative'.
   4 module Language.Symantic.Lib.Applicative where
   5
   6 import Control.Applicative (Applicative)
   7 import Prelude hiding (Functor(..), (<$>), Applicative(..), id, const)
   8 import qualified Control.Applicative as Applicative
   9 import qualified Data.Function as Fun
  10
  11 import Language.Symantic
  12 import Language.Symantic.Lib.Function (a0, b1)
  13 import Language.Symantic.Lib.Functor (Sym_Functor(..), (<$>), f1, f2)
  14
  15 -- * Class 'Sym_Applicative'
  16 type instance Sym Applicative = Sym_Applicative
  17 class Sym_Functor term => Sym_Applicative term where
  18         pure  :: Applicative f => term a -> term (f a)
  19         (<*>) :: Applicative f => term (f (a -> b)) -> term (f a) -> term (f b); infixl 4 <*>
  20         (*>)  :: Applicative f => term (f a) -> term (f b) -> term (f b); infixl 4 *>
  21         (<*)  :: Applicative f => term (f a) -> term (f b) -> term (f a); infixl 4 <*
  22
  23         default pure  :: Sym_Applicative (UnT term) => Trans term => Applicative f => term a -> term (f a)
  24         default (<*>) :: Sym_Applicative (UnT term) => Trans term => Applicative f => term (f (a -> b)) -> term (f a) -> term (f b)
  25         default (*>)  :: Sym_Lambda term => Applicative f => term (f a) -> term (f b) -> term (f b)
  26         default (<*)  :: Sym_Lambda term => Applicative f => term (f a) -> term (f b) -> term (f a)
  27
  28         pure   = trans1 pure
  29         (<*>)  = trans2 (<*>)
  30         x *> y = lam1 Fun.id    <$  x <*> y
  31         x <* y = lam2 Fun.const <$> x <*> y
  32
  33 -- Interpreting
  34 instance Sym_Applicative Eval where
  35         pure  = eval1 Applicative.pure
  36         (<*>) = eval2 (Applicative.<*>)
  37 instance Sym_Applicative View where
  38         pure  = view1 "pure"
  39         (<*>) = viewInfix "<*>" (infixL 4)
  40         (<* ) = viewInfix "<*"  (infixL 4)
  41         ( *>) = viewInfix "*>"  (infixL 4)
  42 instance (Sym_Applicative r1, Sym_Applicative r2, Sym_Lambda r1, Sym_Lambda r2) => Sym_Applicative (Dup r1 r2) where
  43         pure  = dup1 @Sym_Applicative pure
  44         (<*>) = dup2 @Sym_Applicative (<*>)
  45
  46 -- Transforming
  47 instance (Sym_Lambda term, Sym_Applicative term) => Sym_Applicative (BetaT term) where
  48         (<*) = trans2 (<*)
  49         (*>) = trans2 (*>)
  50
  51 -- Typing
  52 instance NameTyOf Applicative where
  53         nameTyOf _c = ["Applicative"] `Mod` "Applicative"
  54 instance FixityOf Applicative
  55 instance ClassInstancesFor Applicative
  56 instance TypeInstancesFor Applicative
  57
  58 -- Compiling
  59 instance Gram_Term_AtomsFor src ss g Applicative
  60 instance (Source src, SymInj ss Applicative) => ModuleFor src ss Applicative where
  61         moduleFor = ["Applicative"] `moduleWhere`
  62          [ "<*>" `withInfixL` 4 := teApplicative_app
  63          , "<*"  `withInfixL` 4 := teApplicative_const
  64          , "*>"  `withInfixL` 4 := teApplicative_tsnoc
  65          ]
  66
  67 -- ** 'Type's
  68 tyApplicative :: Source src => Type src vs a -> Type src vs (Applicative a)
  69 tyApplicative a = tyConstLen @(K Applicative) @Applicative (lenVars a) `tyApp` a
  70
  71 -- ** 'Term's
  72 teApplicative_pure :: TermDef Applicative '[Proxy a, Proxy f] (Applicative f #> (a -> f a))
  73 teApplicative_pure = Term (tyApplicative f1) (a0 ~> f1 `tyApp` a0) $ teSym @Applicative $ lam1 pure
  74
  75 teApplicative_app :: TermDef Applicative '[Proxy a, Proxy b, Proxy f] (Applicative f #> (f (a -> b) -> f a -> f b))
  76 teApplicative_app = Term (tyApplicative f2) (f2 `tyApp` (a0 ~> b1) ~> f2 `tyApp` a0 ~> f2 `tyApp` b1) $ teSym @Applicative $ lam2 (<*>)
  77
  78 teApplicative_const :: TermDef Applicative '[Proxy a, Proxy b1, Proxy f] (Applicative f #> (f a -> f b1 -> f a))
  79 teApplicative_const = Term (tyApplicative f2) (f2 `tyApp` a0 ~> f2 `tyApp` b1 ~> f2 `tyApp` a0) $ teSym @Applicative $ lam2 (<*)
  80
  81 teApplicative_tsnoc :: TermDef Applicative '[Proxy a, Proxy b, Proxy f] (Applicative f #> (f a -> f b -> f b))
  82 teApplicative_tsnoc = Term (tyApplicative f2) (f2 `tyApp` a0 ~> f2 `tyApp` b1 ~> f2 `tyApp` b1) $ teSym @Applicative $ lam2 (*>)