abt- Abstract binding trees for Haskell

Safe HaskellNone




data View v o n φ where Source

v is the type of variables; o is the type of operators parameterized by arities; n is the "higher type"/valence of the term (i.e. a term has n=0, a single binding has n=1, etc.); φ is the functor which interprets the inner structure of the view.


V :: v -> View0 v o φ 
(:\) :: v -> φ n -> View v o (S n) φ 
(:$) :: o ns -> Rec φ ns -> View0 v o φ infixl 2 


Typeable (* -> ([Nat] -> *) -> Nat -> (Nat -> *) -> *) View 

type View0 v o φ = View v o Z φ Source

First order term views.

_ViewOp :: (Choice p, Applicative f, HEq1 o) => o ns -> p (Rec φ ns) (f (Rec φ ns)) -> p (View0 v o φ) (f (View0 v o φ)) Source

A prism to extract arguments from a proposed operator.

_ViewOpHEq1 o ⇒ o ns → Prism' (View0 v o φ) (Rec φ ns)

mapView Source


:: (forall j. φ j -> ψ j)

a natural transformation φ → ψ

-> View v o n φ

a view at φ

-> View v o n ψ 

Views are a (higher) functor.