]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Function.hs
Add term Function.($).
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Function.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for '(->)'.
4 module Language.Symantic.Lib.Function where
5
6 import Prelude hiding (const, flip, id)
7 import qualified Data.Function as Fun
8 import qualified Data.MonoTraversable as MT
9
10 import Language.Symantic
11
12 -- * Class 'Sym_Function'
13 type instance Sym (->) = Sym_Function
14 class Sym_Function term where
15 comp :: term (b -> c) -> term (a -> b) -> term (a -> c); infixr 9 `comp`
16 const :: term a -> term b -> term a
17 flip :: term (a -> b -> c) -> term (b -> a -> c)
18 id :: term a -> term a
19 default comp :: Sym_Function (UnT term) => Trans term => term (b -> c) -> term (a -> b) -> term (a -> c)
20 default const :: Sym_Function (UnT term) => Trans term => term a -> term b -> term a
21 default flip :: Sym_Function (UnT term) => Trans term => term (a -> b -> c) -> term (b -> a -> c)
22 default id :: Sym_Function (UnT term) => Trans term => term a -> term a
23 comp = trans2 comp
24 const = trans2 const
25 flip = trans1 flip
26 id = trans1 id
27
28 -- Interpreting
29 instance Sym_Function Eval where
30 comp = eval2 (Fun..)
31 const = eval2 Fun.const
32 flip = eval1 Fun.flip
33 id = eval1 Fun.id
34 instance Sym_Function View where
35 comp = viewInfix "." (infixR 9)
36 const = view2 "const"
37 flip = view1 "flip"
38 id = view1 "id"
39 instance (Sym_Function r1, Sym_Function r2) => Sym_Function (Dup r1 r2) where
40 comp = dup2 @Sym_Function comp
41 const = dup2 @Sym_Function const
42 flip = dup1 @Sym_Function flip
43 id = dup1 @Sym_Function id
44
45 -- Transforming
46 instance (Sym_Function term, Sym_Lambda term) => Sym_Function (BetaT term)
47
48 -- Typing
49 instance NameTyOf (->) where
50 nameTyOf _c = [] `Mod` "->"
51 instance ClassInstancesFor (->) where
52 proveConstraintFor _c (TyApp _ q (TyApp _ z _r))
53 | Just HRefl <- proj_ConstKiTy @_ @(->) z
54 = case () of
55 _ | Just HRefl <- proj_ConstKiTy @_ @Functor q -> Just Dict
56 | Just HRefl <- proj_ConstKiTy @_ @Applicative q -> Just Dict
57 | Just HRefl <- proj_ConstKiTy @_ @Monad q -> Just Dict
58 _ -> Nothing
59 proveConstraintFor _c (TyApp _ q (TyApp _ (TyApp _ z _a) b))
60 | Just HRefl <- proj_ConstKiTy @_ @(->) z
61 = case () of
62 _ | Just HRefl <- proj_ConstKiTy @_ @Monoid q
63 , Just Dict <- proveConstraint (q `tyApp` b) -> Just Dict
64 | Just HRefl <- proj_ConstKiTy @_ @MT.MonoFunctor q -> Just Dict
65 _ -> Nothing
66 proveConstraintFor _c _q = Nothing
67 instance TypeInstancesFor (->)
68
69 -- Compiling
70 instance Gram_Term_AtomsFor src ss g (->)
71 instance (Source src, SymInj ss (->)) => ModuleFor src ss (->) where
72 moduleFor = ["Function"] `moduleWhere`
73 [ "const" := teFunction_const
74 , "flip" := teFunction_flip
75 , "id" := teFunction_id
76 , "." `withInfixR` 9 := teFunction_compose
77 , "$" `withInfixR` 0 := teFunction_apply
78 ]
79
80 -- ** 'Type's
81 tyFun :: Source src => LenInj vs => Type src vs (->)
82 tyFun = tyConst @(K (->)) @(->)
83
84 a0 :: Source src => LenInj vs => KindInj (K a) =>
85 Type src (Proxy a ': vs) a
86 a0 = tyVar "a" varZ
87
88 b1 :: Source src => LenInj vs => KindInj (K b) =>
89 Type src (a ': Proxy b ': vs) b
90 b1 = tyVar "b" $ VarS varZ
91
92 c2 :: Source src => LenInj vs => KindInj (K c) =>
93 Type src (a ': b ': Proxy c ': vs) c
94 c2 = tyVar "c" $ VarS $ VarS varZ
95
96 -- ** 'Term's
97 teFunction_compose :: TermDef (->) '[Proxy a, Proxy b, Proxy c] (() #> ((b -> c) -> (a -> b) -> (a -> c)))
98 teFunction_compose = Term noConstraint ((b1 ~> c2) ~> (a0 ~> b1) ~> (a0 ~> c2)) $ teSym @(->) $ lam2 comp
99
100 teFunction_const :: TermDef (->) '[Proxy a, Proxy b] (() #> (a -> b -> a))
101 teFunction_const = Term noConstraint (a0 ~> b1 ~> a0) $ teSym @(->) $ lam2 const
102
103 teFunction_flip :: TermDef (->) '[Proxy a, Proxy b, Proxy c] (() #> ((a -> b -> c) -> (b -> a -> c)))
104 teFunction_flip = Term noConstraint ((a0 ~> b1 ~> c2) ~> (b1 ~> a0 ~> c2)) $ teSym @(->) $ lam1 flip
105
106 teFunction_id :: TermDef (->) '[Proxy a] (() #> (a -> a))
107 teFunction_id = Term noConstraint (a0 ~> a0) $ teSym @(->) $ lam1 id
108
109 teFunction_apply :: TermDef (->) '[Proxy a, Proxy b] (() #> ((a -> b) -> a -> b))
110 teFunction_apply = Term noConstraint ((a0 ~> b1) ~> a0 ~> b1) $ teSym @(->) apply