Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Canonical representation of polymorphic functions over containers (http://stackoverflow.com/a/34346484/477476)
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.