{-# LANGUAGE PolyKinds #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Symantic for 'Traversable'. module Language.Symantic.Lib.Traversable where import Prelude hiding (traverse) import qualified Data.Traversable as Traversable import Language.Symantic import Language.Symantic.Lib.Applicative (tyApplicative) import Language.Symantic.Lib.Function (a0, b1) import Language.Symantic.Lib.Functor (f2) -- * Class 'Sym_Traversable' type instance Sym Traversable = Sym_Traversable class Sym_Traversable term where traverse :: Traversable t => Applicative f => term (a -> f b) -> term (t a) -> term (f (t b)) default traverse :: Sym_Traversable (UnT term) => Trans term => Traversable t => Applicative f => term (a -> f b) -> term (t a) -> term (f (t b)) traverse = trans2 traverse -- Interpreting instance Sym_Traversable Eval where traverse = eval2 Traversable.traverse instance Sym_Traversable View where traverse = view2 "traverse" instance (Sym_Traversable r1, Sym_Traversable r2) => Sym_Traversable (Dup r1 r2) where traverse = dup2 @Sym_Traversable traverse -- Transforming instance (Sym_Traversable term, Sym_Lambda term) => Sym_Traversable (BetaT term) -- Typing instance FixityOf Traversable instance ClassInstancesFor Traversable instance TypeInstancesFor Traversable -- Compiling instance Gram_Term_AtomsFor src ss g Traversable instance (Source src, SymInj ss Traversable) => ModuleFor src ss Traversable where moduleFor = ["Traversable"] `moduleWhere` [ "traverse" := teTraversable_traverse ] -- ** 'Type's tyTraversable :: Source src => Type src vs a -> Type src vs (Traversable a) tyTraversable a = tyConstLen @(K Traversable) @Traversable (lenVars a) `tyApp` a -- * 'Term's teTraversable_traverse :: TermDef Traversable '[Proxy a, Proxy b, Proxy f, Proxy t] (Traversable t # Applicative f #> ((a -> f b) -> t a -> f (t b))) teTraversable_traverse = Term (tyTraversable t # tyApplicative f2) ((a0 ~> f2 `tyApp` b1) ~> t `tyApp` a0 ~> f2 `tyApp` (t `tyApp` b1)) $ teSym @Traversable $ lam2 traverse where t :: Source src => LenInj vs => KindInj (K t) => Type src (Proxy a ': Proxy b ': Proxy c ': Proxy t ': vs) t t = tyVar "t" $ VarS $ VarS $ VarS varZ