Base64 Encoding in Idris

Our program demonstrates base64 encoding and decoding in Idris. Here’s the full source code:

module Main

import Data.String
import Data.Buffer
import Data.Buffer.Encode

main : IO ()
main = do
    let data = "abc123!?$*&()'-=@~"

    -- Standard base64 encoding
    let sEnc = base64Encode data
    putStrLn sEnc

    -- Standard base64 decoding
    case base64Decode sEnc of
        Right sDec -> putStrLn $ fastUnpack sDec
        Left err -> putStrLn $ "Decoding error: " ++ err

    putStrLn ""

    -- URL-safe base64 encoding
    let uEnc = base64UrlEncode data
    putStrLn uEnc

    -- URL-safe base64 decoding
    case base64UrlDecode uEnc of
        Right uDec -> putStrLn $ fastUnpack uDec
        Left err -> putStrLn $ "Decoding error: " ++ err

where
    base64Encode : String -> String
    base64Encode = fastPack . encode Base64 . fastPack

    base64Decode : String -> Either String Buffer
    base64Decode = decode Base64 . fastPack

    base64UrlEncode : String -> String
    base64UrlEncode = fastPack . encode Base64Url . fastPack

    base64UrlDecode : String -> Either String Buffer
    base64UrlDecode = decode Base64Url . fastPack

This program uses the Data.Buffer.Encode module, which provides functions for base64 encoding and decoding. Here’s a breakdown of what the code does:

1. We define a string that we’ll encode and decode.

2. We use base64Encode to perform standard base64 encoding. This function converts the string to a buffer, encodes it, and then converts the result back to a string.

3. For decoding, we use base64Decode. This function returns an Either String Buffer, where Left contains an error message if decoding fails, and Right contains the decoded buffer if successful.

4. We repeat the process with base64UrlEncode and base64UrlDecode for URL-safe base64 encoding and decoding.

5. The fastPack and fastUnpack functions are used to convert between String and Buffer types efficiently.

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

$ idris Base64Encoding.idr -o base64_encoding
$ ./base64_encoding
YWJjMTIzIT8kKiYoKSctPUB+
abc123!?$*&()'-=@~

YWJjMTIzIT8kKiYoKSctPUB-
abc123!?$*&()'-=@~

The output shows that both standard and URL-safe base64 encoding produce slightly different results (note the trailing + vs -), but both decode back to the original string as expected.

In Idris, error handling is typically done using the Either type, which we’ve used here for the decoding functions. This allows for more explicit error handling compared to some other languages.