printf_in_idris.md

OK... this has very weak support for the %f format specification, but it works:

module IO.Printf

toOctal : Int -> String
toOctal n = let (q, r) = (div n 8, mod n 8) in
            case q == 0 of
              True => show r
              False => toOctal q ++ show r

data Caps = Up | Down

toHex' : Int -> Int -> String
toHex' offset n = let (q, r) = (div n 16, mod n 16) in
                  case q == 0 of
                    True  => show' r
                    False => toHex' offset q ++ show' r
                  where
                    show' : Int -> String
                    show' r = case r < 10 of
                                True  => show r
                                False => singleton $ chr (r + offset)

toHex : Caps -> Int -> String
toHex Up n   = toHex' 55 n
toHex Down n = toHex' 87 n

-- This is a recursive type for describing a format specifier
-- For example, "%s is %d%" would be expressed as
-- Str (Lit " is " (Number (Lit "%" End)))
data Format = Number Format
            | Oct Format
            | Hex Caps Format
            | Str Format
            | Chr Format
            | Dbl Format
            | Lit String Format
            | End

-- This function takes a format specifier in the form of a string
-- and recursively builds and returns a Format type
total
toFormat : (string : List Char) -> Format
toFormat string = case string of
                    [] => End
                    ('%' :: 'd' :: chars)        => Number $ toFormat chars
                    ('%' :: 'o' :: chars)        => Oct $ toFormat chars
                    ('%' :: '#' :: 'o' :: chars) => Lit "0" $ Oct $ toFormat chars
                    ('%' :: 'x' :: chars)        => Hex Down $ toFormat chars
                    ('%' :: '#' :: 'x' :: chars) => Lit "0x" $ Hex Down $ toFormat chars
                    ('%' :: 'X' :: chars)        => Hex Up (toFormat chars)
                    ('%' :: '#' :: 'X' :: chars) => Lit "0X" $ Hex Up $ toFormat chars
                    ('%' :: 's' :: chars)        => Str $ toFormat chars
                    ('%' :: 'c' :: chars)        => Chr $ toFormat chars
                    ('%' :: 'f' :: chars)        => Dbl $ toFormat chars
                    (c :: chars)                 => case toFormat chars of
                                                      Lit lit chars' => Lit (strCons c lit) chars'
                                                      fmt => Lit (strCons c "") fmt

-- This is also a recursive type that describes
-- the return type of the printf function
PrintfType : Format -> Type
PrintfType (Number fmt)   = (i : Int) -> PrintfType fmt
PrintfType (Oct fmt)      = (i : Int) -> PrintfType fmt
PrintfType (Hex caps fmt) = (i : Int) -> PrintfType fmt
PrintfType (Str fmt)      = (str : String) -> PrintfType fmt
PrintfType (Chr fmt)      = (char : Char) -> PrintfType fmt
PrintfType (Dbl fmt)      = (dbl : Double) -> PrintfType fmt
PrintfType (Lit str fmt)  = PrintfType fmt
PrintfType End            = String

-- This function is a helper for the printf function
-- and is actually the one that does all the work by
-- accumulating the output string
printfHelper : (fmt : Format) -> (acc : String) -> PrintfType fmt
printfHelper (Number fmt) acc   = \i => printfHelper fmt $ acc ++ show i
printfHelper (Oct fmt) acc      = \i => printfHelper fmt $ acc ++ toOctal i
printfHelper (Hex caps fmt) acc = \i => printfHelper fmt $ acc ++ toHex caps i
printfHelper (Str fmt) acc      = \s => printfHelper fmt $ acc ++ s
printfHelper (Chr fmt) acc      = \c => printfHelper fmt $ pack $ unpack acc ++ [c]
printfHelper (Dbl fmt) acc      = \d => printfHelper fmt $ acc ++ show d
printfHelper (Lit str fmt) acc  = printfHelper fmt $ acc ++ str
printfHelper End acc            = acc

-- The actual interface and point of entry, it passes an empty
-- accumulator to the helper above
printf : (fmt : String) -> PrintfType $ toFormat $ unpack fmt
printf fmt = printfHelper _ ""

And when I test that implementation it works:

danielle@danielles-MacBook-Pro-2 ~/p/i/src> idris
     ____    __     _
    /  _/___/ /____(_)____
    / // __  / ___/ / ___/     Version 1.2.0
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
 /___/\__,_/_/  /_/____/       Type :? for help

Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Idris> :module IO.Printf
*IO/Printf> printf "%f is an approximation to %s" 3.14 "pi"
"3.14 is an approximation to pi" : String

But when I try to start moving in a direction to support width and precision specifiers I run into trouble:

data SearchResults = NoSpec
                   | FSpec Nat Nat (List Char)

total
searchNumericSpecs : List Char -> SearchResults
searchNumericSpecs chars = case span (/= 'f') chars of
                             (_, [])               => NoSpec
                             ([], 'f' :: chars')   => FSpec 0 6 chars'
                             (spec, 'f' :: chars') => FSpec 0 6 chars'
                             (_, _)                => NoSpec

total
toFormat : (string : List Char) -> Format
toFormat string = case string of
                    [] => End
                    ('%' :: 'd' :: chars)        => Number $ toFormat chars
                    ('%' :: 'o' :: chars)        => Oct $ toFormat chars
                    ('%' :: '#' :: 'o' :: chars) => Lit "0" $ Oct $ toFormat chars
                    ('%' :: 'x' :: chars)        => Hex Down $ toFormat chars
                    ('%' :: '#' :: 'x' :: chars) => Lit "0x" $ Hex Down $ toFormat chars
                    ('%' :: 'X' :: chars)        => Hex Up (toFormat chars)
                    ('%' :: '#' :: 'X' :: chars) => Lit "0X" $ Hex Up $ toFormat chars
                    ('%' :: 's' :: chars)        => Str $ toFormat chars
                    ('%' :: 'c' :: chars)        => Chr $ toFormat chars
                    ('%' :: chars)               => case searchNumericSpecs chars of
                                                      NoSpec                  => Lit "%" $ toFormat chars
                                                      FSpec width prec chars' => Dbl $ toFormat chars'
                    (c :: chars)                 => case toFormat chars of
                                                      Lit lit chars' => Lit (strCons c lit) chars'
                                                      fmt => Lit (strCons c "") fmt

That compiles and satisfies the type checker, but everything is broken now:

danielle@danielles-MacBook-Pro-2 ~/p/i/src> idris
     ____    __     _
    /  _/___/ /____(_)____
    / // __  / ___/ / ___/     Version 1.2.0
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
 /___/\__,_/_/  /_/____/       Type :? for help

Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Idris> :module IO.Printf
*IO/Printf> printf "%f is an approximation to %s" 3.14 "pi"
(input):1:1-47:printf "%f is an approximation to %s" does not have a function type (PrintfType (toFormat (unpack "%f is an approximation to %s")))
*IO/Printf> printf "%s" "WAT?"
(input):1:1-18:printf "%s" does not have a function type (PrintfType (toFormat (unpack "%s")))

Cause

When you compile your updated Idris file, you should see a warning like this:

printf.idr:51:1:Printf.toFormat is possibly not total due to recursive path Printf.toFormat --> Printf.toFormat --> Printf.toFormat

(Line number might be different on your end.)

The reason is this line:

                    ('%' :: chars)               => case searchNumericSpecs chars of
                                                      NoSpec                  => Lit "%" $ toFormat chars
                                                      FSpec width prec chars' => Dbl $ toFormat chars' ---- this line

You're performing a recursive call to toFormat with chars' which you obtained from searchNumericSpecs. Unfortunately, Idris' termination checker won't be able to figure out that chars' is in fact shorter than chars, which would be needed for termination.

The reason why you're seeing the strange output in the REPL is as follows: To figure out how many arguments printf takes, the Idris compiler has to evaluate the toFormat function at compile-time. It will refuse to do so if it believes the function is not total (that which the warning message indicated).

Quick fix

There's a "quick fix", namely just to assert totality/termination:

                    ('%' :: chars)               => case searchNumericSpecs chars of
                                                      NoSpec                  => Lit "%" $ toFormat chars
                                                      FSpec width prec chars' => Dbl $ assert_total $ toFormat chars'

This will make your examples go through:

*printf> printf "%f is an approximation to %s" 3.14 "pi"
"3.14 is an approximation to pi" : String                                                                                                                                                                                                                                      
*printf> printf "%s" "WAT?"
"WAT?" : String

Proper fix

Prove termination of this function properly, without assert_total. I'm afraid my Idris knowledge is not advanced enough for this. It would probably require returning a dependent pair from searchNumericSpecs that proved that the resulting list is strictly shorter than the input list.

Hey @larsrh, thanks for linking to this gist.

Hi @quephird, that's an interesting one. I'm by no means an experienced Idris user but maybe we can tackle this problem together. Let's see if we can rewrite toFormat to make it total. To do this we will employ views.

Views—just like pattern matching—allow us to destructure data. Using pattern matching we can destructure values by applying their constructors.

head : List a -> Maybe a
head [] = Nothing
head (x :: _) = Just x

Views on the other hand allow us to destructure data in a more arbitrary way.

import Data.List.Views

last : List a -> Maybe a
last xs with (snocList xs)
  last [] | Empty = Nothing
  last (ys ++ [y]) | (Snoc rec) = Just y

Here, snocList is a covering function of the SnocList view. It gives us another perspective for looking at lists; namely, from the other end.

Let's define a recursive view over a list of characters. There are three cases:

• the list is empty,
• the list consists of a literal with the rest appended, or
• the list consists of a formatting pattern with the rest appended.

data FormatString : List Char -> Type where
  FormatStringEmpty : FormatString []
  FormatStringLit : (rec : FormatString rest) ->
                    FormatString (lit ++ rest)
  FormatStringFormat : (rec : FormatString rest) ->
                       FormatString ('%' :: format ++ rest)

We need to supplement our view with a covering function. It will take a List Char as an argument and return a FormatString for the given list.

formatString : (str : List Char) -> FormatString str
formatString [] = FormatStringEmpty
formatString [x] = FormatStringLit {lit = [x]} FormatStringEmpty
formatString ('%' :: 'd' :: xs) =
  FormatStringFormat {format = ['d']} $ formatString xs
formatString ('%' :: 'f' :: xs) =
  FormatStringFormat {format = ['f']} $ formatString xs
formatString ('%' :: 'o' :: xs) =
  FormatStringFormat {format = ['o']} $ formatString xs
formatString ('%' :: '#' :: 'o' :: xs) =
  FormatStringFormat {format = ['#', 'o']} $ formatString xs
formatString ('%' :: '#' :: 'x' :: xs) =
  FormatStringFormat {format = ['#', 'x']} $ formatString xs
formatString ('%' :: 's' :: xs) =
  FormatStringFormat {format = ['s']} $ formatString xs
formatString ('%' :: (x :: xs)) = formatStringFormatHelper [x] xs
formatString (x :: xs) = formatStringLitHelper [x] xs

First two cases cover strings with zero or one character. They cannot contain any formatting patterns. Then we address a number of cases for fixed-width formatting patterns. It's kind of repetitive; I'm wondering if it could be simplified. The last two cases are triggered when we run into a formatting pattern or a literal.

formatStringFormatHelper : (prefix : List Char) ->
                           (rest : List Char) ->
                           FormatString ('%' :: prefix ++ rest)
formatStringFormatHelper prefix [] = FormatStringFormat FormatStringEmpty
formatStringFormatHelper prefix ('f' :: xs) =
  rewrite appendAssociative prefix ['f'] xs in
          FormatStringFormat {format = prefix ++ ['f']} $ formatString xs
formatStringFormatHelper prefix (x :: xs) =
  rewrite appendAssociative prefix [x] xs in
          formatStringFormatHelper (prefix ++ [x]) xs

Here we keep taking elements from rest and appending them to prefix until we hit an 'f'. Everything up to and including 'f' becomes our formatting pattern. Then we continue parsing the rest with formatString. I hope it's a satisfactory approximation of your searchNumericSpecs.

We need to rewrite some types in order to satisfy the type checker. appendAssociative allows us to prove that the following equality holds.

(prefix ++ ['f']) ++ xs = prefix ++ 'f' :: xs

Patterns such as "%03f" are covered. Now we need to parse literals for as long as we don't hit a '%'.

formatStringLitHelper : (prefix : List Char) ->
                        (rest : List Char) ->
                        FormatString (prefix ++ rest)
formatStringLitHelper prefix [] = FormatStringLit FormatStringEmpty
formatStringLitHelper prefix ('%' :: xs) =
  FormatStringLit $ formatString ('%' :: xs)
formatStringLitHelper prefix (x :: xs) =
  rewrite appendAssociative prefix [x] xs in
          formatStringLitHelper (prefix ++ [x]) xs

If you take a close look you'll notice that the structure of formatStringFormatHelper and formatStringLitHelper is very similar. Keep appending characters to prefix until you see a '%'. Then fall back to formatString.

Three functions above are mutually recursive. Because of that they have to be defined in a single mutual block.

The resulting covering function is total and we can use it in toFormat.

toFormat : (string : List Char) -> Format
toFormat string with (formatString string)
  toFormat [] | FormatStringEmpty = ?rhs_1
  toFormat (lit ++ rest) | (FormatStringLit rec) = ?rhs_2
  toFormat ('%' :: (format ++ rest)) | (FormatStringFormat rec) = ?rhs_3

Our input string is either empty or consists of two parts: a literal or a formating string, postfixed with the rest. Let's finish the definition.

toFormat : (string : List Char) -> Format
toFormat string with (formatString string)
  toFormat [] | FormatStringEmpty = End
  toFormat (lit ++ rest) | (FormatStringLit rec) =
    Lit (pack lit) $ toFormat rest | rec
  toFormat ('%' :: (format ++ rest)) | (FormatStringFormat rec) =
    fmt (toFormat rest | rec)
    where fmt : Format -> Format
          fmt = case format of
                  ['d'] => Number
                  ['o'] => Oct
                  ['x'] => Hex Down
                  ['#', 'o'] => Lit "0" . Oct
                  ['#', 'x'] => Lit "0x" . Hex Down
                  ['s'] => Str
                  ['f'] => Dbl
                  other => case searchNumericSpecs other of
                             NoSpec => Lit $ pack other
                             (FSpec w p _) => Dbl

In the last case—when none of the constant formatting patterns match—I'm attempting to parse it as a floating point pattern. If it doesn't work I give up and return a literal, just as your code does.

The resulting function is total.

*IO.Printf> :total toFormat
IO.Printf.toFormat is Total
*IO.Printf> PrintfType $ toFormat $ unpack "%03f is an approximation to %s"
Double -> String -> String : Type

As a closing note, I can't recommend enough the TDD with Idris book. Chapter 10 discusses views in depth.

I hope this helps! As I wrote above, I'm new to all of this and I welcome all feedback and improvement ideas.