Methods in Idris

module Main

import System.IO

-- Idris supports records, which are similar to structs
record Rect : Type where
  constructor MkRect
  width : Int
  height : Int

-- This 'area' function takes a Rect as an argument
area : Rect -> Int
area r = r.width * r.height

-- Here's another function that takes a Rect
perim : Rect -> Int
perim r = 2 * r.width + 2 * r.height

main : IO ()
main = do
  -- Create a Rect instance
  let r = MkRect 10 5
  
  -- Call the functions we defined
  putStrLn $ "area: " ++ show (area r)
  putStrLn $ "perim: " ++ show (perim r)
  
  -- In Idris, we don't need to worry about pointer vs value semantics
  -- as it's a purely functional language
  putStrLn $ "area: " ++ show (area r)
  putStrLn $ "perim: " ++ show (perim r)

In Idris, we define a Rect record which is similar to a struct. Instead of methods, we define functions that take a Rect as an argument.

The area function calculates the area of a rectangle:

area : Rect -> Int
area r = r.width * r.height

And the perim function calculates its perimeter:

perim : Rect -> Int
perim r = 2 * r.width + 2 * r.height

In the main function, we create a Rect instance and call our functions:

main : IO ()
main = do
  let r = MkRect 10 5
  putStrLn $ "area: " ++ show (area r)
  putStrLn $ "perim: " ++ show (perim r)

Idris is a purely functional language, so we don’t need to worry about pointer vs value semantics. There’s no distinction between calling methods on a value or a pointer.

To run this program, you would save it as a .idr file and use the Idris compiler:

$ idris -o rect rect.idr
$ ./rect
area: 50
perim: 30
area: 50
perim: 30

In Idris, we use records and functions instead of structs and methods, but the core concept of bundling data with operations on that data remains the same.

Structs in Idris

Interfaces in Idris

Learn X By Example

Title here

Methods in Idris