Maps in Idris

To create an empty map, use nil and the Map type in Idris.

module Main

import Data.Map
import Prelude
import Control.Monad

main : IO ()
main = do
    let m : Map String Int
    putStrLn $ "Map: " ++ show m

    let m' = insert "k1" 7 (insert "k2" 13 m)
    putStrLn $ "Map: " ++ show m'

    let v1 = maybe 0 id (lookup "k1" m')
    putStrLn $ "v1: " ++ show v1

    let v3 = maybe 0 id (lookup "k3" m')
    putStrLn $ "v3: " ++ show v3

    let len = size m'
    putStrLn $ "len: " ++ show len

    let m'' = delete "k2" m'
    putStrLn $ "Map: " ++ show m''

    let m''' = empty
    putStrLn $ "Map: " ++ show m'''

    let prs = isJust $ lookup "k2" m'
    putStrLn $ "prs: " ++ show prs

    let n = fromList [("foo", 1), ("bar", 2)]
    putStrLn $ "Map: " ++ show n

    let n2 = fromList [("foo", 1), ("bar", 2)]
    when (n == n2) $ putStrLn "n == n2"
  • Maps in Idris are implemented using the Data.Map module.
  • To create an empty map, use Map.
  • We can set key/value pairs using the insert function.
  • Use the show function to print the map.
  • To get a value for a key, use the lookup function, which returns a Maybe type.
  • The size function returns the number of key/value pairs in a map.
  • The delete function removes key/value pairs from a map.
  • The empty function clears all key/value pairs from the map.
  • To check if a key exists, use the isJust function combined with lookup.
  • You can declare and initialize a new map using fromList.
  • We can compare two maps using the == operator.