]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Traversable.hs
Add TyApp pattern synonyms (:$) and (:@).
[haskell/symantic.git] / 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