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 (TyConst _ _ q :$ f:@_r)
  53          | Just HRefl <- proj_ConstKiTy @_ @(->) f
  54          = case () of
  55                  _ | Just Refl <- proj_Const @Functor     q -> Just Dict
  56                    | Just Refl <- proj_Const @Applicative q -> Just Dict
  57                    | Just Refl <- proj_Const @Monad       q -> Just Dict
  58                  _ -> Nothing
  59         proveConstraintFor _c (tq@(TyConst _ _ q) :$ f:@_a:@b)
  60          | Just HRefl <- proj_ConstKiTy @_ @(->) f
  61          = case () of
  62                  _ | Just Refl <- proj_Const @Monoid q
  63                    , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
  64                    | Just Refl <- proj_Const @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