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"/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.

Constructors

V :: v -> View0 v o φ

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

(:$) :: o ns -> Rec φ ns -> View0 v o φ infixl 2

Instances

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

type View0 v o φ = View v o Z φ

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 φ))

A prism to extract arguments from a proposed operator.

_ViewOp ∷ HEq1 o ⇒ o ns → Prism' (View0 v o φ) (Rec φ ns)

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.