symantic-lib/Language/Symantic/Lib/Traversable.hs

   1 {-# LANGUAGE PolyKinds #-}
   2 {-# LANGUAGE UndecidableInstances #-}
   3 {-# OPTIONS_GHC -fno-warn-orphans #-}
   4 -- | Symantic for 'Traversable'.
   5 module Language.Symantic.Lib.Traversable where
   6
   7 import Prelude hiding (traverse)
   8 import qualified Data.Traversable as Traversable
   9
  10 import Language.Symantic
  11 import Language.Symantic.Lib.Applicative (tyApplicative)
  12 import Language.Symantic.Lib.Function (a0, b1)
  13 import Language.Symantic.Lib.Functor (f2)
  14
  15 -- * Class 'Sym_Traversable'
  16 type instance Sym Traversable = Sym_Traversable
  17 class Sym_Traversable term where
  18         traverse :: Traversable t => Applicative f => term (a -> f b) -> term (t a) -> term (f (t b))
  19         default traverse :: Sym_Traversable (UnT term) => Trans term => Traversable t => Applicative f => term (a -> f b) -> term (t a) -> term (f (t b))
  20         traverse = trans2 traverse
  21
  22 -- Interpreting
  23 instance Sym_Traversable Eval where
  24         traverse = eval2 Traversable.traverse
  25 instance Sym_Traversable View where
  26         traverse = view2 "traverse"
  27 instance (Sym_Traversable r1, Sym_Traversable r2) => Sym_Traversable (Dup r1 r2) where
  28         traverse = dup2 @Sym_Traversable traverse
  29
  30 -- Transforming
  31 instance (Sym_Traversable term, Sym_Lambda term) => Sym_Traversable (BetaT term)
  32
  33 -- Typing
  34 instance NameTyOf Traversable where
  35         nameTyOf _c = ["Traversable"] `Mod` "Traversable"
  36 instance FixityOf Traversable
  37 instance ClassInstancesFor Traversable
  38 instance TypeInstancesFor Traversable
  39
  40 -- Compiling
  41 instance Gram_Term_AtomsFor src ss g Traversable
  42 instance (Source src, SymInj ss Traversable) => ModuleFor src ss Traversable where
  43         moduleFor = ["Traversable"] `moduleWhere`
  44          [ "traverse" := teTraversable_traverse
  45          ]
  46
  47 -- ** 'Type's
  48 tyTraversable :: Source src => Type src vs a -> Type src vs (Traversable a)
  49 tyTraversable a = tyConstLen @(K Traversable) @Traversable (lenVars a) `tyApp` a
  50
  51 -- * 'Term's
  52 teTraversable_traverse :: TermDef Traversable '[Proxy a, Proxy b, Proxy f, Proxy t] (Traversable t # Applicative f #> ((a -> f b) -> t a -> f (t b)))
  53 teTraversable_traverse = Term (tyTraversable t # tyApplicative f2) ((a0 ~> f2 `tyApp` b1) ~> t `tyApp` a0 ~> f2 `tyApp` (t `tyApp` b1)) $ teSym @Traversable $ lam2 traverse
  54         where
  55         t :: Source src => LenInj vs => KindInj (K t) => Type src (Proxy a ': Proxy b ': Proxy c ': Proxy t ': vs) t
  56         t = tyVar "t" $ VarS $ VarS $ VarS varZ