For in Idris

Idris provides several ways to create loops and iterate over collections. Here are some basic types of loops in Idris.

import Data.String

main : IO ()
main = do
    -- The most basic type, with a single condition.
    let i = 1
    loop1 i
    where
        loop1 : Int -> IO ()
        loop1 i = 
            if i <= 3
            then do
                putStrLn $ show i
                loop1 (i + 1)
            else pure ()

    -- A classic initial/condition/after loop using recursion.
    loop2 0
    where
        loop2 : Int -> IO ()
        loop2 j = 
            if j < 3
            then do
                putStrLn $ show j
                loop2 (j + 1)
            else pure ()

    -- Another way of accomplishing the basic "do this N times" iteration
    -- is using `replicateM_`.
    replicateM_ 3 $ \i -> 
        putStrLn $ "range " ++ show i

    -- Idris doesn't have a direct equivalent to Go's infinite loop,
    -- but we can create one using recursion.
    let infiniteLoop = do
        putStrLn "loop"
        pure ()  -- In this case, we're just exiting after one iteration

    infiniteLoop

    -- You can also use list comprehension for iteration with filtering.
    let oddNumbers = [n | n <- [0..5], n `mod` 2 /= 0]
    traverse_ (\n -> putStrLn $ show n) oddNumbers

To run the program, save it as for.idr and use the Idris interpreter:

$ idris for.idr -o for
$ ./for
1
2
3
0
1
2
range 0
range 1
range 2
loop
1
3
5

In Idris, we use recursion and higher-order functions like replicateM_ to achieve looping behavior. The traverse_ function is used to iterate over a list and perform an action for each element. List comprehensions provide a concise way to generate lists with conditions.

We’ll see some other forms of iteration later when we look at list processing, IO operations, and other data structures.

Constants in Idris

If Else in Idris

Learn X By Example

Title here

For in Idris