Canonical representation of polymorphic functions over containers (http://stackoverflow.com/a/34346484/477476)

Shapeshifting.agda

open import Data.Product
open import Function using (_∘_; id)

data Cont : Set₁ where
  _<|_ : (S : Set) → (P : S → Set) → Cont

[_]C : Cont → Set → Set
[ S <| P ]C X = Σ[ s ∈ S ] (P s → X)


mapC : ∀ C {X Y} → (X → Y) → [ C ]C X → [ C ]C Y
mapC (S <| P) f (s , k) = s , f ∘ k

Poly : ∀ (C C′ : Cont) → Set₁
Poly C C′ = ∀ {X} → [ C ]C X → [ C′ ]C X

record ShapeShifter (S : Set) (P : S → Set) (S′ : Set) (P′ : S′ → Set) : Set where
  field
    toS : S → S′
    fromP : (s : S) → P′ (toS s) → P s

shapeShifter : ∀ {S S′ P P′} → Poly (S <| P) (S′ <| P′) → ShapeShifter S P S′ P′
shapeShifter {S} {S′} {P} {P′} f =
    record { toS = λ s → proj₁ (shifty s)
           ; fromP = λ s → proj₂ (shifty s)
           }
  where
    shifty : (x : S) → [ S′ <| P′ ]C (P x)
    shifty s = f (s , id)