{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
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)
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))
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 (<$)
instance (Sym_Functor term, Sym_Lambda term) => Sym_Functor (BetaT term) where
(<$>) = trans2 (<$>)
(<$) = trans2 (<$)
instance NameTyOf Functor where
nameTyOf _c = ["Functor"] `Mod` "Functor"
instance FixityOf Functor
instance ClassInstancesFor Functor
instance TypeInstancesFor Functor
instance Gram_Term_AtomsFor src ss g Functor
instance (Source src, SymInj ss Functor) => ModuleFor src ss Functor where
moduleFor = ["Functor"] `moduleWhere`
[ "fmap" := teFunctor_fmap
, "<$" `withInfixL` 4 := teFunctor_const
, "<$>" `withInfixL` 4 := teFunctor_fmap_infix
]
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 => LenInj vs => KindInj (K f) =>
Type src (a ': Proxy f ': vs) f
f1 = tyVar "f" $ VarS varZ
f2 :: Source src => LenInj vs => KindInj (K f) =>
Type src (a ': b ': Proxy f ': vs) f
f2 = tyVar "f" $ VarS $ VarS varZ
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 (<$)