Struct Embedding in Idris

module Main

import Data.String

-- Define a record type 'Base'
record Base where
  constructor MkBase
  num : Int

-- Define a method for Base
describe : Base -> String
describe b = "base with num=" ++ show b.num

-- Define a record type 'Container' that includes Base
record Container where
  constructor MkContainer
  base : Base
  str : String

-- Main function
main : IO ()
main = do
  -- Create a Container instance
  let co = MkContainer (MkBase 1) "some name"

  -- Access fields directly
  putStrLn $ "co={num: " ++ show co.base.num ++ ", str: " ++ co.str ++ "}"

  -- Access fields using the full path
  putStrLn $ "also num: " ++ show co.base.num

  -- Call the describe method
  putStrLn $ "describe: " ++ describe co.base

  -- Define a interface (type class in Idris)
  interface Describer a where
    describe' : a -> String

  -- Implement Describer for Container
  implementation Describer Container where
    describe' c = describe c.base

  -- Use the interface
  let d : Describer Container => Container = co
  putStrLn $ "describer: " ++ describe' d

In Idris, struct embedding is achieved through record types. The concept is similar, but the syntax and implementation details differ. Here’s an explanation of the key points:

We define Base and Container as record types.
The describe function is defined separately for Base, rather than as a method.
Container includes Base as a field, which is similar to embedding in Go.
We can access fields of Base through Container using dot notation, like co.base.num.
Idris uses type classes instead of interfaces. We define a Describer type class and implement it for Container.
The Describer implementation for Container delegates to the describe function of Base.

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

$ idris StructEmbedding.idr -o StructEmbedding
$ ./StructEmbedding
co={num: 1, str: some name}
also num: 1
describe: base with num=1
describer: base with num=1

This example demonstrates how Idris can achieve similar functionality to Go’s struct embedding using record types and type classes.

Enums in Idris

Generics in Idris

Learn X By Example

Title here

Struct Embedding in Idris