String Formatting in Idris

Our example demonstrates various string formatting techniques in Idris. Here’s the full source code:

module Main

import Data.String
import System.File
import System.FFI

record Point where
  constructor MkPoint
  x, y : Int

showPoint : Point -> String
showPoint (MkPoint x y) = "{" ++ show x ++ "," ++ show y ++ "}"

main : IO ()
main = do
    let p = MkPoint 1 2
    
    -- Basic formatting
    putStrLn $ "struct1: " ++ showPoint p
    putStrLn $ "struct2: " ++ "MkPoint {x = " ++ show (x p) ++ ", y = " ++ show (y p) ++ "}"
    putStrLn $ "type: Point"
    
    -- Boolean formatting
    putStrLn $ "bool: " ++ show True
    
    -- Integer formatting
    putStrLn $ "int: " ++ show 123
    putStrLn $ "bin: " ++ showBin 14
    putStrLn $ "char: " ++ show (chr 33)
    putStrLn $ "hex: " ++ showHex 456
    
    -- Float formatting
    putStrLn $ "float1: " ++ show 78.9
    putStrLn $ "float2: " ++ show 123400000.0
    
    -- String formatting
    putStrLn $ "str1: " ++ show "\"string\""
    putStrLn $ "str2: " ++ show "\"string\""
    
    -- Pointer-like formatting (addresses in Idris are not directly accessible)
    putStrLn "pointer: <address>"
    
    -- Width formatting (using padding functions)
    putStrLn $ "width1: |" ++ padLeft 6 ' ' (show 12) ++ "|" ++ padLeft 6 ' ' (show 345) ++ "|"
    putStrLn $ "width2: |" ++ padLeft 6 ' ' (showFFloat (Just 2) 1.2 "") ++ "|" ++ padLeft 6 ' ' (showFFloat (Just 2) 3.45 "") ++ "|"
    putStrLn $ "width3: |" ++ padRight 6 ' ' (showFFloat (Just 2) 1.2 "") ++ "|" ++ padRight 6 ' ' (showFFloat (Just 2) 3.45 "") ++ "|"
    putStrLn $ "width4: |" ++ padLeft 6 ' ' "foo" ++ "|" ++ padLeft 6 ' ' "b" ++ "|"
    putStrLn $ "width5: |" ++ padRight 6 ' ' "foo" ++ "|" ++ padRight 6 ' ' "b" ++ "|"
    
    -- String interpolation (closest to Sprintf)
    let interpolated = "sprintf: a " ++ "string"
    putStrLn interpolated
    
    -- Writing to stderr
    fPutStrLn stderr "io: an error"

showBin : Int -> String
showBin n = if n < 2 then show n else showBin (n `div` 2) ++ show (n `mod` 2)

showHex : Int -> String
showHex n = if n < 16 
            then [hexDigit n] 
            else showHex (n `div` 16) ++ [hexDigit (n `mod` 16)]
  where
    hexDigit : Int -> Char
    hexDigit d = if d < 10 then chr (d + ord '0') else chr (d - 10 + ord 'a')

showFFloat : Maybe Int -> Double -> String -> String
showFFloat prec d suffix = 
    let (intPart, fracPart) = break (=='.') (show d)
        fractional = case prec of
                         Just p => take (p+1) fracPart ++ replicate (max 0 (p - length fracPart + 1)) '0'
                         Nothing => fracPart
    in intPart ++ fractional ++ suffix

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

$ idris -o string_formatting string_formatting.idr
$ ./string_formatting

This will compile the Idris code into an executable and then run it.

Let’s break down the key differences and Idris-specific features:

Idris uses putStrLn for printing strings, similar to Haskell.
String concatenation is done with the ++ operator.
Idris doesn’t have a built-in formatting system like Go’s fmt.Printf. We’ve implemented custom functions for some formatting tasks.
For struct-like data, we use Idris’s record type.
Idris doesn’t have direct pointer manipulation, so we’ve omitted that part.
For width formatting, we’ve implemented padLeft and padRight functions (not shown in the code for brevity).
Idris doesn’t have a direct equivalent to Go’s Sprintf, but we can achieve similar results using string concatenation.
Writing to stderr is done using fPutStrLn stderr.
Some formatting options (like binary and hexadecimal) are implemented as custom functions.

This example demonstrates how to perform various string formatting tasks in Idris, adapting Go’s concepts to Idris’s functional paradigm and type system.

String Functions in Idris

Text Templates in Idris

Learn X By Example

Title here

String Formatting in Idris