Abt.Types.View

Documentation

data View v o n φ where

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.

Constructors

V :: v -> View v o Z φ

(:\) :: v -> φ n -> View v o (S n) φ

(:$) :: o ns -> HList φ ns -> View v o Z φ

mapView

Arguments

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

a natural transformation φ → ψ

-> View v o n φ

a view at φ

-> View v o n ψ

Views are a (higher) functor.