[Haskell] The initial view on typed sprintf and sscanf

[oleg at okmij.org]

We demonstrate typed sprintf and typed sscanf sharing the same
formatting specification. Our solution is surprisingly trivial: it
defines a simple embedded domain-specific language of formatting
patterns. The functions sprintf and sscanf are two interpreters of the
language, to build or parse a string according to the given
pattern. Our solution relies only on GADTs. We demonstrate that
lambda-abstractions at the type level are expressible already in the
Hindley-Milner type system; GADT with the included polymorphic
recursion help us use the abstractions.

The typed sprintf takes the formatting specification and several
arguments and returns the formatted string. The types and the number
of arguments depend on the formatting specification. Conversely, the
typed sscanf parses a string according to the formatting
specification, passing parsed data to a consumer function. Again, the
number and the types of the arguments to the consumer depend on the
formatting specification. The typed sprintf problem has been
investigated extensively: the first solution was shown by Danvy; more
solutions were proposed by Hinze and Asai. The typed scanf problem
received significantly less attention, if any. It seems that the
implementation of the typed sprintf and sscanf sharing the same
formatting specification has not been known.

Here are a few examples of the typed sprintf and sscanf

> tp1 = sprintf $ lit "Hello world"
> -- "Hello world"
> ts1 = sscanf "Hello world" (lit "Hello world")  ()
> -- Just ()

> tp2 = sprintf (lit "Hello " ^ lit "world" ^ char) '!'
> -- "Hello world!"
> ts2 = sscanf "Hello world!" (lit "Hello " ^ lit "world" ^ char) id
> -- Just '!'

> fmt3 = lit "The value of " ^ char ^ lit " is " ^ int
> tp3 = sprintf fmt3 'x' 3
> -- "The value of x is 3"
> ts3 = sscanf "The value of x is 3" fmt3 (\c i -> (c,i))
> -- Just ('x',3)

A formatting specification is built by connecting primitive
specifications (such as lit "string", int, char) with (^). We observe
that whereas 
     sprintf $ lit "Hello world"
has the type String, 
     sprintf $ lit "The value of " ^ char ^ lit " is " ^ int
has the type Char -> Int -> String. Likewise, the type of the consumer
of the values parsed by sscanf varies with the formatting specification.
The example of tp3 and ts3 demonstrates that sprintf and sscanf can
indeed use exactly the same formatting specification, which
is a first-class value.

Printf and scanf are present in many languages (e.g., C and Haskell);
in most of the cases, they are not type-safe: the type checker does
not stop the programmer from passing to printf more or fewer arguments
than required by the formatting string. OCaml supports typed sprintf
and sscanf, which relies on a particular weird typing of these
functions, resulting in formatting specifications being not first
class. Our sscanf has exactly the same interface as that in OCaml,
modulo weird typing.

The complete code of the typed sprintf and sscanf with more examples
is available at
	http://okmij.org/ftp/Haskell/PrintScan.hs
It can be used in Haskell programs as it is; it is trivial to arrange
it in a Haskell library or Hackage package.


Our implementation is based on the observation of Hinze (Ralf
Hinze. Functional Pearl: Formatting: a class act. JFP, 13(5):935-944,
September 2003) that the formatting specification is a `type
transformer', a functor. For example, the formatting specification
'int' is associated with a functor transforming a type 't' to a type
'Int -> t'. Hinze represented functors in Curry style; the
functor associated with 'int' is then (Int ->).  However, a more
direct, Church-style representation is also possible.  Let us consider
a type "F a b" where "F" is a binary type constructor, "a" is a type
variable, and "b" is a type that may include one or more occurrences of
"a". That type is essentially a type abstraction, the type-level
lambda-function. To apply the function to an argument, we unify "a"
with the argument; the second parameter of "F" is the result of the
application. This is the standard emulation of lambda-calculus in
Prolog.

Based on this observation, we define the language of formatting
specifications as follows:

> data F a b where
>     FLit :: String -> F a a
>     FInt :: F a (Int -> a)
>     FChr :: F a (Char -> a)
>     (:^) :: F b c -> F a b -> F a c

> (^)  = (:^)
> lit  = FLit
> int  = FInt

The type of (:^) expresses the inverse functional composition of two
type-level lambdas; one may read "F" as `big lambda'.

The formatting specification can be interpreted in two different ways,
for printing and for parsing. The types of the interpreters are pleasingly
symmetric:

> intp :: F a b -> (String -> a) -> b
> intp (FLit str) k = k str
> intp FChr       k = \x -> k [x]
> intp (a :^ b)   k = intp a (\sa -> intp b (\sb -> k (sa ++ sb)))


> ints :: F a b -> String -> b -> Maybe (a,String)
> ints (FLit str) inp x = maybe Nothing (\inp' -> Just (x,inp')) $ 
>                           prefix str inp
> ints FChr (c:inp) f = Just (f c,inp)
> ints FChr "" f      = Nothing
> ints (a :^ b) inp f = maybe Nothing (\(vb,inp') -> ints b inp' vb) $ 
> 		          ints a inp f


The printing interpretation implements Asai's accumulator-less alternative to
Danvy's functional unparsing:
	http://pllab.is.ocha.ac.jp/~asai/papers/tr07-1.ps.gz
The printing interpretation of (a :^ b) is string concatenation in CPS form.

The sprintf and sscanf are then simple wrappers:

> sprintf :: F String b -> b
> sprintf fmt = intp fmt id

> sscanf :: String -> F a b -> b -> Maybe a
> sscanf inp fmt f = maybe Nothing (Just . fst) $ ints fmt inp f

The problem of the typed printf and scanf over the same formatting
specification has been posed by Chung-chieh Shan in a discussion with
Kenichi Asai and Yukiyoshi Kameyama. I'm grateful to them for
inspiration.