Skip to content

Instantly share code, notes, and snippets.

@UlfNorell
Created August 30, 2018 07:41
Show Gist options
  • Save UlfNorell/97431837733a9a71e58c363540bd099e to your computer and use it in GitHub Desktop.
Save UlfNorell/97431837733a9a71e58c363540bd099e to your computer and use it in GitHub Desktop.
Reversing an ascending list in Agda
-- Reversing an ascending list in Agda.
-- Challenge by @arntzenius: https://twitter.com/arntzenius/status/1034919539467677696
module AscList where
-- We'll go without libraries to make things clearer.
flip : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → (A → B → C) → B → A → C
flip f x y = f y x
-- Step one is to define ordered lists. We'll roughly follow Conor McBride's approach
-- from How to keep your neighbours in order [1].
-- Lists will be indexed by upper and lower bounds. An unrestricted list is bounded by
-- -∞ and ∞.
data Bound (A : Set) : Set where
-∞ : Bound A
# : A → Bound A
∞ : Bound A
-- Any relation on A can be lifted to Bound A. As expected -∞ is smaller than anything
-- and ∞ is bigger than anything.
data liftB {A : Set} (_≤_ : A → A → Set) : (lo hi : Bound A) → Set where
-∞≤ : ∀ {b} → liftB _≤_ -∞ b
≤∞ : ∀ {b} → liftB _≤_ b ∞
# : ∀ {x y} → x ≤ y → liftB _≤_ (# x) (# y)
-- Now, given an A and a relation _≤_ over A we can define ascending lists of A's.
module _ {A : Set} (_≤_ : A → A → Set) where
private _≤ᵇ_ = liftB _≤_
data AscendingList (lo hi : Bound A) : Set where
-- The empty list can have any bounds you like, as long as the lower bound is
-- below the upper bound.
nil : lo ≤ᵇ hi → AscendingList lo hi
-- When consing an element x onto a list xs, x needs to be above the expected
-- lower bound and x should be a lower bound for xs. The upper bound is enforced
-- by the fact that xs is bounded by # x and hi.
cons : (x : A) → lo ≤ᵇ # x → AscendingList (# x) hi → AscendingList lo hi
-- A descending list is an ascending list with the ordering flipped, but we also need to flip
-- -∞ and ∞.
flipB : ∀ {A} → Bound A → Bound A
flipB -∞ = ∞
flipB (# x) = # x
flipB ∞ = -∞
DescendingList : {A : Set} (_≤_ : A → A → Set) (lo hi : Bound A) → Set
DescendingList _≤_ hi lo = AscendingList (flip _≤_) (flipB hi) (flipB lo)
-- So, DescendingList _≤_ ∞ -∞ = AscendingList (flip _≤_) -∞ ∞.
-- Those are all the definitions we'll need. Time to get reversing.
module _ {A : Set} {_≤_ : A → A → Set} where
-- Let's have some nicer names for ordering proofs. The proofs in the ascending list
-- will be _≤ᵇ_s, and the proofs in the descending list should be _≥ᵇ_s.
private
_≤ᵇ_ = liftB _≤_
_≥ᵇ_ = λ hi lo → liftB (flip _≤_) (flipB hi) (flipB lo)
-- Turning one into the other is straightforward.
flip≤ᵇ : ∀ {lo hi} → lo ≤ᵇ hi → hi ≥ᵇ lo
flip≤ᵇ -∞≤ = ≤∞
flip≤ᵇ ≤∞ = -∞≤
flip≤ᵇ (# lt) = # lt
-- Usually the helper function for reverse takes two lists, one to be reversed and one
-- accumulator for the result. In this case however we need to be a bit more precise about
-- the bounds, so we take the element that should go next on the accumulator as a separate
-- argument. This also makes shuffling of the proofs easier: note how the x≤y proof moves
-- from the cons cell of y to the cons cell of x when reversing.
rev : ∀ {lo hi} (x : A) → AscendingList _≤_ (# x) hi → DescendingList _≤_ (# x) lo →
DescendingList _≤_ hi lo
rev x (nil x≤hi) ys = cons x (flip≤ᵇ x≤hi) ys
rev x (cons y x≤y xs) ys = rev y xs (cons x (flip≤ᵇ x≤y) ys)
-- Since rev requires an element we need to match on the list in reverse as well. Fortunately
-- the nil case is trivial.
reverse : ∀ {lo hi} → AscendingList _≤_ lo hi → DescendingList _≤_ hi lo
reverse (nil lt) = nil (flip≤ᵇ lt)
reverse (cons x lt xs) = rev x xs (nil (flip≤ᵇ lt))
-- [1] https://scholar.google.se/scholar?q=How+to+Keep+Your+Neighbours+in+Order
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment