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:
We import necessary modules:
Data.List
for sorting functions andData.String
for string operations.We define a custom
Person
data type with a name (String) and an age (Int).We implement
lenCmp
, a comparison function for string lengths. This uses the built-incompare
function.We implement
ageCmp
, a comparison function forPerson
objects based on their age.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 usingsortBy ageCmp
.
- We create a list of fruits and sort it using
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.