Universe lifting for type families
Some functors such as option and list are universe polymorphic. Unlike
type polymorphism where option α is a function application and reasoning and
generalizations that apply to functions can be used, option.{u} and option.{v}
are not one function applied to two universe names but one polymorphic definition
instantiated twice. This means that whatever works on option.{u} is hard
to transport over to option.{v}. uliftable is an attempt at improving the situation.
uliftable option.{u} option.{v} gives us a generic and composable way to use
option.{u} in a context that requires option.{v}. It is often used in tandem with
ulift but the two are purposefully decoupled.
Main definitions
uliftableclass
Tags
universe polymorphism functor
Given a universe polymorphic type family M.{u} : Type u₁ → Type
u₂, this class convert between instantiations, from
M.{u} : Type u₁ → Type u₂ to M.{v} : Type v₁ → Type v₂ and back
The most common practical use uliftable (together with up), this function takes x : M.{u} α and lifts it
to M.{max u v} (ulift.{v} α)
Equations
The most common practical use of uliftable (together with up), this function takes x : M.{max u v} (ulift.{v} α)
and lowers it to M.{u} α
Equations
convenient shortcut to avoid manipulating ulift
Equations
- uliftable.adapt_up x f = uliftable.up x >>= f ∘ ulift.down
convenient shortcut to avoid manipulating ulift
Equations
- uliftable.adapt_down x f = uliftable.down (x >>= uliftable.up ∘ f)
map function that moves up universes
Equations
- uliftable.up_map f x = (f ∘ ulift.down) <$> uliftable.up x
map function that moves down universes
Equations
- uliftable.down_map f x = uliftable.down ((ulift.up ∘ f) <$> x)
Equations
- id.uliftable = {congr := λ (α : Type u_1) (β : Type u_2) (F : α ≃ β), F}
for specific state types, this function helps to create a uliftable instance
Equations
- state_t.uliftable' F = {congr := λ (α : Type u₀) (β : Type u₁) (G : α ≃ β), state_t.equiv (F.Pi_congr (λ (_x : s), uliftable.congr m m' (G.prod_congr F)))}
Equations
for specific reader monads, this function helps to create a uliftable instance
Equations
- reader_t.uliftable' F = {congr := λ (α : Type u_1) (β : Type u_2) (G : α ≃ β), reader_t.equiv (F.Pi_congr (λ (_x : s), uliftable.congr m m' G))}
Equations
for specific continuation passing monads, this function helps to create a uliftable instance
Equations
- cont_t.uliftable' F = {congr := λ (α : Type u_1) (β : Type u_2), cont_t.equiv (uliftable.congr m m' F)}
Equations
for specific writer monads, this function helps to create a uliftable instance
Equations
- writer_t.uliftable' F = {congr := λ (α : Type (max u_1 u_2)) (β : Type (max u_3 u_4)) (G : α ≃ β), writer_t.equiv (uliftable.congr m m' (G.prod_congr F))}