{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Symantic for '(->)'. module Language.Symantic.Lib.Function where import Prelude hiding (const, flip, id) import qualified Data.Function as Fun import qualified Data.MonoTraversable as MT import Language.Symantic -- * Class 'Sym_Function' type instance Sym (->) = Sym_Function class Sym_Function term where comp :: term (b -> c) -> term (a -> b) -> term (a -> c); infixr 9 `comp` const :: term a -> term b -> term a flip :: term (a -> b -> c) -> term (b -> a -> c) id :: term a -> term a default comp :: Sym_Function (UnT term) => Trans term => term (b -> c) -> term (a -> b) -> term (a -> c) default const :: Sym_Function (UnT term) => Trans term => term a -> term b -> term a default flip :: Sym_Function (UnT term) => Trans term => term (a -> b -> c) -> term (b -> a -> c) default id :: Sym_Function (UnT term) => Trans term => term a -> term a comp = trans2 comp const = trans2 const flip = trans1 flip id = trans1 id -- Interpreting instance Sym_Function Eval where comp = eval2 (Fun..) const = eval2 Fun.const flip = eval1 Fun.flip id = eval1 Fun.id instance Sym_Function View where comp = viewInfix "." (infixR 9) const = view2 "const" flip = view1 "flip" id = view1 "id" instance (Sym_Function r1, Sym_Function r2) => Sym_Function (Dup r1 r2) where comp = dup2 @Sym_Function comp const = dup2 @Sym_Function const flip = dup1 @Sym_Function flip id = dup1 @Sym_Function id -- Transforming instance (Sym_Function term, Sym_Lambda term) => Sym_Function (BetaT term) -- Typing instance NameTyOf (->) where nameTyOf _c = [] `Mod` "->" instance ClassInstancesFor (->) where proveConstraintFor _c (TyApp _ q (TyApp _ z _r)) | Just HRefl <- proj_ConstKiTy @_ @(->) z = case () of _ | Just HRefl <- proj_ConstKiTy @_ @Functor q -> Just Dict | Just HRefl <- proj_ConstKiTy @_ @Applicative q -> Just Dict | Just HRefl <- proj_ConstKiTy @_ @Monad q -> Just Dict _ -> Nothing proveConstraintFor _c (TyApp _ q (TyApp _ (TyApp _ z _a) b)) | Just HRefl <- proj_ConstKiTy @_ @(->) z = case () of _ | Just HRefl <- proj_ConstKiTy @_ @Monoid q , Just Dict <- proveConstraint (q `tyApp` b) -> Just Dict | Just HRefl <- proj_ConstKiTy @_ @MT.MonoFunctor q -> Just Dict _ -> Nothing proveConstraintFor _c _q = Nothing instance TypeInstancesFor (->) -- Compiling instance Gram_Term_AtomsFor src ss g (->) instance (Source src, SymInj ss (->)) => ModuleFor src ss (->) where moduleFor = ["Function"] `moduleWhere` [ "const" := teFunction_const , "flip" := teFunction_flip , "id" := teFunction_id , "." `withInfixR` 9 := teFunction_compose , "$" `withInfixR` 0 := teFunction_apply ] -- ** 'Type's tyFun :: Source src => LenInj vs => Type src vs (->) tyFun = tyConst @(K (->)) @(->) a0 :: Source src => LenInj vs => KindInj (K a) => Type src (Proxy a ': vs) a a0 = tyVar "a" varZ b1 :: Source src => LenInj vs => KindInj (K b) => Type src (a ': Proxy b ': vs) b b1 = tyVar "b" $ VarS varZ c2 :: Source src => LenInj vs => KindInj (K c) => Type src (a ': b ': Proxy c ': vs) c c2 = tyVar "c" $ VarS $ VarS varZ -- ** 'Term's teFunction_compose :: TermDef (->) '[Proxy a, Proxy b, Proxy c] (() #> ((b -> c) -> (a -> b) -> (a -> c))) teFunction_compose = Term noConstraint ((b1 ~> c2) ~> (a0 ~> b1) ~> (a0 ~> c2)) $ teSym @(->) $ lam2 comp teFunction_const :: TermDef (->) '[Proxy a, Proxy b] (() #> (a -> b -> a)) teFunction_const = Term noConstraint (a0 ~> b1 ~> a0) $ teSym @(->) $ lam2 const teFunction_flip :: TermDef (->) '[Proxy a, Proxy b, Proxy c] (() #> ((a -> b -> c) -> (b -> a -> c))) teFunction_flip = Term noConstraint ((a0 ~> b1 ~> c2) ~> (b1 ~> a0 ~> c2)) $ teSym @(->) $ lam1 flip teFunction_id :: TermDef (->) '[Proxy a] (() #> (a -> a)) teFunction_id = Term noConstraint (a0 ~> a0) $ teSym @(->) $ lam1 id teFunction_apply :: TermDef (->) '[Proxy a, Proxy b] (() #> ((a -> b) -> a -> b)) teFunction_apply = Term noConstraint ((a0 ~> b1) ~> a0 ~> b1) $ teSym @(->) apply