module Abt.Types.View
( View(..)
, View0
, _ViewOp
, mapView
) where
import Abt.Class.HEq1
import Abt.Types.Nat
import Control.Applicative
import Data.Profunctor
import Data.Vinyl
data View (v ∷ *) (o ∷ [Nat] → *) (n ∷ Nat) (φ ∷ Nat → *) where
V ∷ v → View0 v o φ
(:\) ∷ v → φ n → View v o (S n) φ
(:$) ∷ o ns → Rec φ ns → View0 v o φ
infixl 2 :$
type View0 v o φ = View v o Z φ
mapView
∷ (∀ j. φ j → ψ j)
→ View v o n φ
→ View v o n ψ
mapView η = \case
V v → V v
v :\ e → v :\ η e
o :$ es → o :$ η <<$>> es
_ViewOp
∷ ( Choice p
, Applicative f
, HEq1 o
)
⇒ o ns
→ p (Rec φ ns) (f (Rec φ ns))
→ p (View0 v o φ) (f (View0 v o φ))
_ViewOp o = dimap fro (either pure (fmap (o :$))) . right'
where
fro = \case
o' :$ es | Just Refl ← heq1 o o' → Right es
e → Left e