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

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