{-# LANGUAGE PolyKinds #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Symantic for 'Functor'. module Language.Symantic.Lib.Functor where import Data.Functor (Functor) import Prelude hiding (Functor(..), (<$>)) import qualified Data.Function as Fun import qualified Data.Functor as Functor import Language.Symantic import Language.Symantic.Lib.Function (a0, b1) -- * Class 'Sym_Functor' type instance Sym Functor = Sym_Functor class Sym_Functor term where fmap :: Functor f => term (a -> b) -> term (f a) -> term (f b) default fmap :: Sym_Functor (UnT term) => Trans term => Functor f => term (a -> b) -> term (f a) -> term (f b) fmap = trans2 fmap (<$>) :: (Sym_Functor term, Functor f) => term (a -> b) -> term (f a) -> term (f b); infixl 4 <$> (<$>) = fmap (<$) :: Functor f => term a -> term (f b) -> term (f a); infixl 4 <$ default (<$) :: Sym_Lambda term => Functor f => term a -> term (f b) -> term (f a) (<$) x = fmap (lam (Fun.const x)) -- Interpreting instance Sym_Functor Eval where fmap = eval2 Functor.fmap (<$) = eval2 (Functor.<$) instance Sym_Functor View where fmap = view2 "fmap" (<$>) = viewInfix "<$>" (infixL 4) (<$) = viewInfix "<$" (infixL 4) instance (Sym_Functor r1, Sym_Functor r2) => Sym_Functor (Dup r1 r2) where fmap = dup2 @Sym_Functor fmap (<$) = dup2 @Sym_Functor (<$) -- Transforming instance (Sym_Functor term, Sym_Lambda term) => Sym_Functor (BetaT term) where (<$>) = trans2 (<$>) (<$) = trans2 (<$) -- Typing instance FixityOf Functor instance ClassInstancesFor Functor instance TypeInstancesFor Functor -- Compiling instance Gram_Term_AtomsFor src ss g Functor instance (Source src, Inj_Sym ss Functor) => ModuleFor src ss Functor where moduleFor = ["Functor"] `moduleWhere` [ "fmap" := teFunctor_fmap , "<$" `withInfixL` 4 := teFunctor_const , "<$>" `withInfixL` 4 := teFunctor_fmap_infix ] -- ** 'Type's tyFunctor :: Source src => Type src vs a -> Type src vs (Functor a) tyFunctor a = tyConstLen @(K Functor) @Functor (lenVars a) `tyApp` a f1 :: Source src => Inj_Len vs => Inj_Kind (K f) => Type src (a ': Proxy f ': vs) f f1 = tyVar "f" $ VarS varZ f2 :: Source src => Inj_Len vs => Inj_Kind (K f) => Type src (a ': b ': Proxy f ': vs) f f2 = tyVar "f" $ VarS $ VarS varZ -- ** 'Term's teFunctor_fmap, teFunctor_fmap_infix :: TermDef Functor '[Proxy a, Proxy b, Proxy f] (Functor f #> ((a -> b) -> f a -> f b)) teFunctor_fmap = Term (tyFunctor f2) ((a0 ~> b1) ~> f2 `tyApp` a0 ~> f2 `tyApp` b1) $ teSym @Functor $ lam2 fmap teFunctor_fmap_infix = Term (tyFunctor f2) ((a0 ~> b1) ~> f2 `tyApp` a0 ~> f2 `tyApp` b1) $ teSym @Functor $ lam2 (<$>) teFunctor_const :: TermDef Functor '[Proxy a, Proxy b, Proxy f] (Functor f #> (a -> f b -> f a)) teFunctor_const = Term (tyFunctor f2) (a0 ~> f2 `tyApp` b1 ~> f2 `tyApp` a0) $ teSym @Functor $ lam2 (<$)