abt- Abstract binding trees for Haskell

Safe HaskellSafe-Inferred




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" 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 -> View v o Z φ 
(:\) :: v -> φ n -> View v o (S n) φ 
(:$) :: o ns -> HList φ ns -> View v o Z φ 

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.