Range Over Built in Idris

Here we use foreach to sum the numbers in a list.

module Main

import Data.List

main : IO ()
main = do
    let nums = [2, 3, 4]
    let sum = foldl (+) 0 nums
    putStrLn $ "sum: " ++ show sum

    -- `foreach` on lists provides both the index and value for each entry. 
    -- Above we didn’t need the index, so we ignored it. 
    -- Sometimes we actually want the indexes though.

    mapM_ (\(i, num) => 
              when (num == 3) $ 
                putStrLn $ "index: " ++ show i) 
          (indexed nums)

    -- `foreach` on map iterates over key/value pairs.
    let kvs = fromList [("a", "apple"), ("b", "banana")]
    mapM_ (\(k, v) => putStrLn $ k ++ " -> " ++ v) $ toList kvs

    -- `foreach` can also iterate over just the keys of a map.
    mapM_ (\k => putStrLn $ "key: " ++ k) $ toKeys kvs

    -- `foreach` on strings iterates over characters.
    mapM_ (\(i, c) => putStrLn $ show i ++ " " ++ show c) $ indexed "go"

To run the program, save the code in a file (e.g., RangeOverBuiltInTypes.idr), and use the Idris compiler to run it.

$ idris --execute RangeOverBuiltInTypes.idr
sum: 9
index: 1
a -> apple
b -> banana
key: a
key: b
0 'g'
1 'o'

Now that we can iterate over built-in types in Idris, let’s learn more about the language.

Recursion in Idris

Pointers in Idris

Learn X By Example

Title here

Range Over Built in Idris