If Else in Idris

Our first example demonstrates branching with if and else in Idris. This is straightforward and similar to many other programming languages.

module Main

import System.IO

main : IO ()
main = do
    -- Here's a basic example.
    if 7 `mod` 2 == 0 then
        putStrLn "7 is even"
    else
        putStrLn "7 is odd"

    -- You can have an `if` statement without an else.
    if 8 `mod` 4 == 0 then
        putStrLn "8 is divisible by 4"

    -- Logical operators like `&&` and `||` are often useful in conditions.
    if 8 `mod` 2 == 0 || 7 `mod` 2 == 0 then
        putStrLn "either 8 or 7 are even"

    -- In Idris, we can use let bindings to introduce local variables.
    -- These are available in the current and all subsequent branches.
    let num = 9
    if num < 0 then
        putStrLn $ show num ++ " is negative"
    else if num < 10 then
        putStrLn $ show num ++ " has 1 digit"
    else
        putStrLn $ show num ++ " has multiple digits"

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

$ idris IfElse.idr -o ifelse
$ ./ifelse
7 is odd
8 is divisible by 4
either 8 or 7 are even
9 has 1 digit

Note that in Idris, you don’t need parentheses around conditions, but indentation is significant. The then and else keywords are required for each branch.

Idris doesn’t have a ternary operator, so you’ll need to use a full if statement even for basic conditions. However, Idris has pattern matching which can often be used as an alternative to complex if-else structures.

One key difference in Idris is its strong type system and support for dependent types. While this example doesn’t showcase these features, they allow for more powerful and precise conditionals in more complex programs.

For in Idris

Switch in Idris

Learn X By Example

Title here

If Else in Idris