{- Task: Implement insertion sort. For instance, sort (5 ∷ 3 ∷ 10 ∷ 1 ∷ []) will yield the list 1 ∷ 3 ∷ 5 ∷ 10 ∷ []. -} data _⊎_ (X Y : Set) : Set where left : X → X ⊎ Y right : Y → X ⊎ Y -- "Let a set A be fixed." module _ (A : Set) (_≤_ : A → A → Set) -- "x ≤ y" is the type of -- witnesses that x is less than -- or equal to y (cmp? : (x y : A) → (x ≤ y) ⊎ (y ≤ x)) where -- For instance, in the case that "A" is the type ℕ -- and "_≤_" is the usual ordering relation, -- "cmp? 5 10" should be something of the form "left ...", -- "cmp? 10 5" should be something of the form "right ...". data List : Set where [] : List _∷_ : A → List → List -- If the list "ys" is already sorted (ascendingly), -- the list "insert x ys" should be the same as "ys", -- but with the element "x" inserted at the appropriate -- location. -- For instance: "insert 5 (2 ∷ 10 ∷ 20 ∷ [])" should -- yield "2 ∷ 5 ∷ 10 ∷ 20 ∷ []". insert : A → List → List insert x [] = x ∷ [] insert x (y ∷ ys) with cmp? x y ... | left x≤y = x ∷ (y ∷ ys) ... | right y≤x = y ∷ insert x ys -- There are two options: The correct result might by -- (a) x ∷ y ∷ ys (this is correct if x ≤ y) -- (b) y ∷ insert x ys (this is correct if y ≤ x) sort : List → List sort [] = [] sort (x ∷ xs) = insert x (sort xs)