]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Functor.hs
Rename inj_* -> *Inj.
[haskell/symantic.git] / 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 FixityOf Functor
48 instance ClassInstancesFor Functor
49 instance TypeInstancesFor Functor
50
51 -- Compiling
52 instance Gram_Term_AtomsFor src ss g Functor
53 instance (Source src, SymInj ss Functor) => ModuleFor src ss Functor where
54 moduleFor = ["Functor"] `moduleWhere`
55 [ "fmap" := teFunctor_fmap
56 , "<$" `withInfixL` 4 := teFunctor_const
57 , "<$>" `withInfixL` 4 := teFunctor_fmap_infix
58 ]
59
60 -- ** 'Type's
61 tyFunctor :: Source src => Type src vs a -> Type src vs (Functor a)
62 tyFunctor a = tyConstLen @(K Functor) @Functor (lenVars a) `tyApp` a
63
64 f1 :: Source src => LenInj vs => KindInj (K f) =>
65 Type src (a ': Proxy f ': vs) f
66 f1 = tyVar "f" $ VarS varZ
67
68 f2 :: Source src => LenInj vs => KindInj (K f) =>
69 Type src (a ': b ': Proxy f ': vs) f
70 f2 = tyVar "f" $ VarS $ VarS varZ
71
72 -- ** 'Term's
73 teFunctor_fmap, teFunctor_fmap_infix :: TermDef Functor '[Proxy a, Proxy b, Proxy f] (Functor f #> ((a -> b) -> f a -> f b))
74 teFunctor_fmap = Term (tyFunctor f2) ((a0 ~> b1) ~> f2 `tyApp` a0 ~> f2 `tyApp` b1) $ teSym @Functor $ lam2 fmap
75 teFunctor_fmap_infix = Term (tyFunctor f2) ((a0 ~> b1) ~> f2 `tyApp` a0 ~> f2 `tyApp` b1) $ teSym @Functor $ lam2 (<$>)
76
77 teFunctor_const :: TermDef Functor '[Proxy a, Proxy b, Proxy f] (Functor f #> (a -> f b -> f a))
78 teFunctor_const = Term (tyFunctor f2) (a0 ~> f2 `tyApp` b1 ~> f2 `tyApp` a0) $ teSym @Functor $ lam2 (<$)