Sorting in Idris

Our example demonstrates sorting in Idris. We’ll look at sorting for built-in types first.

import Data.List
import Data.String

main : IO ()
main = do
    -- Sorting functions work for any type that implements the Ord interface.
    -- For strings, we can use the built-in sort function.
    let strs = ["c", "a", "b"]
    let sortedStrs = sort strs
    putStrLn $ "Strings: " ++ show sortedStrs

    -- An example of sorting integers.
    let ints = [7, 2, 4]
    let sortedInts = sort ints
    putStrLn $ "Ints:    " ++ show sortedInts

    -- We can also check if a list is already in sorted order.
    let isSorted = sorted sortedInts
    putStrLn $ "Sorted:  " ++ show isSorted

To run this program, save it to a file (e.g., sorting.idr) and use the Idris interpreter:

$ idris sorting.idr -o sorting
$ ./sorting
Strings: ["a","b","c"]
Ints:    [2,4,7]
Sorted:  True

In this Idris example, we’re using the Data.List module which provides sorting functionality. The sort function is used to sort both strings and integers. The sorted function checks if a list is already in sorted order.

Idris, being a purely functional language, doesn’t modify lists in-place. Instead, sort returns a new sorted list. This is different from some imperative languages where sorting might be done in-place.

The Ord interface in Idris is similar to the concept of ordered types in other languages. Any type that implements Ord can be sorted using these functions.

Note that Idris doesn’t have a direct equivalent to Go’s slices package. In Idris, these operations are typically done on lists, which are a fundamental data structure in the language.