module Main

import System.REPL

-- Here's a basic interface for geometric shapes.
interface Geometry a where
  area : a -> Double
  perim : a -> Double

-- For our example we'll implement this interface on
-- 'Rect' and 'Circle' types.
record Rect where
  constructor MkRect
  width, height : Double

record Circle where
  constructor MkCircle
  radius : Double

-- To implement an interface in Idris, we need to create
-- instances for our types. Here we implement 'Geometry' on 'Rect'.
implementation Geometry Rect where
  area r = r.width * r.height
  perim r = 2 * r.width + 2 * r.height

-- The implementation for 'Circle'.
implementation Geometry Circle where
  area c = pi * c.radius * c.radius
  perim c = 2 * pi * c.radius

-- If a function takes an interface type as an argument, then we can call
-- methods that are in the named interface. Here's a
-- generic 'measure' function taking advantage of this
-- to work on any 'Geometry'.
measure : Geometry a => a -> IO ()
measure g = do
  putStrLn $ "Area: " ++ show (area g)
  putStrLn $ "Perimeter: " ++ show (perim g)

main : IO ()
main = do
  let r = MkRect 3 4
  let c = MkCircle 5
  
  -- The 'Circle' and 'Rect' types both
  -- implement the 'Geometry' interface so we can use
  -- instances of these types as arguments to 'measure'.
  measure r
  measure c