Sorting By Functions in Idris

Our example demonstrates how to implement custom sorting in Idris. We’ll sort strings by their length and a custom data type by one of its fields.

import Data.List
import Data.String

-- We define a custom data type for Person
data Person = MkPerson String Int

-- A helper function to compare the lengths of two strings
lenCmp : String -> String -> Ordering
lenCmp a b = compare (length a) (length b)

-- A helper function to compare the ages of two Person objects
ageCmp : Person -> Person -> Ordering
ageCmp (MkPerson _ age1) (MkPerson _ age2) = compare age1 age2

main : IO ()
main = do
    -- Define a list of fruits
    let fruits = ["peach", "banana", "kiwi"]
    
    -- Sort fruits by length
    let sortedFruits = sortBy lenCmp fruits
    putStrLn $ show sortedFruits
    
    -- Define a list of Person objects
    let people = [MkPerson "Jax" 37, MkPerson "TJ" 25, MkPerson "Alex" 72]
    
    -- Sort people by age
    let sortedPeople = sortBy ageCmp people
    putStrLn $ show sortedPeople

In this Idris code:

  1. We import necessary modules: Data.List for sorting functions and Data.String for string operations.

  2. We define a custom Person data type with a name (String) and an age (Int).

  3. We implement lenCmp, a comparison function for string lengths. This uses the built-in compare function.

  4. We implement ageCmp, a comparison function for Person objects based on their age.

  5. In the main function:

    • We create a list of fruits and sort it using sortBy lenCmp.
    • We create a list of Person objects and sort it using sortBy ageCmp.
  6. We use putStrLn $ show ... to print the sorted lists.

Note that Idris uses sortBy from Data.List instead of slices.SortFunc. The sortBy function takes a comparison function and a list, and returns a sorted list.

To run this program, save it as CustomSorting.idr and use the Idris compiler:

$ idris CustomSorting.idr -o CustomSorting
$ ./CustomSorting
["kiwi", "peach", "banana"]
[MkPerson "TJ" 25, MkPerson "Jax" 37, MkPerson "Alex" 72]

This example demonstrates how to implement custom sorting logic in Idris, which can be applied to both built-in types like String and custom data types like Person.