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 (Proxy 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 FixityOf Traversable
  35 instance ClassInstancesFor Traversable
  36 instance TypeInstancesFor Traversable
  37
  38 -- Compiling
  39 instance Gram_Term_AtomsFor src ss g Traversable
  40 instance (Source src, Inj_Sym ss Traversable) => Module src ss Traversable where
  41         module_ _s = [] `moduleWhere`
  42          [ "traverse" := teTraversable_traverse
  43          ]
  44
  45 -- ** 'Type's
  46 tyTraversable :: Source src => Type src vs a -> Type src vs (Traversable a)
  47 tyTraversable a = tyConstLen @(K Traversable) @Traversable (lenVars a) `tyApp` a
  48
  49 -- * 'Term's
  50 teTraversable_traverse :: TermDef Traversable '[Proxy a, Proxy b, Proxy f, Proxy t] (Traversable t # Applicative f #> ((a -> f b) -> t a -> f (t b)))
  51 teTraversable_traverse = Term (tyTraversable t # tyApplicative f2) ((a0 ~> f2 `tyApp` b1) ~> t `tyApp` a0 ~> f2 `tyApp` (t `tyApp` b1)) $ teSym @Traversable $ lam2 traverse
  52         where
  53         t :: Source src => Inj_Len vs => Inj_Kind (K t) => Type src (Proxy a ': Proxy b ': Proxy c ': Proxy t ': vs) t
  54         t = tyVar "t" $ VarS $ VarS $ VarS varZ