5 This page provides a gentle introduction and derivation of <:Printf:>,
6 with sections and arrangement more suitable to a talk.
11 SML does not have `printf`. Could we define it ourselves?
15 val () = printf ("here's an int %d and a real %f.\n", 13, 17.0)
16 val () = printf ("here's three values (%d, %f, %f).\n", 13, 17.0, 19.0)
19 What could the type of `printf` be?
21 This obviously can't work, because SML functions take a fixed number
22 of arguments. Actually they take one argument, but if that's a tuple,
23 it can only have a fixed number of components.
26 == From tupling to currying ==
28 What about currying to get around the typing problem?
32 val () = printf "here's an int %d and a real %f.\n" 13 17.0
33 val () = printf "here's three values (%d, %f, %f).\n" 13 17.0 19.0
36 That fails for a similar reason. We need two types for `printf`.
39 val printf: string -> int -> real -> unit
40 val printf: string -> int -> real -> real -> unit
43 This can't work, because `printf` can only have one type. SML doesn't
44 support programmer-defined overloading.
47 == Overloading and dependent types ==
49 Even without worrying about number of arguments, there is another
50 problem. The type of `printf` depends on the format string.
54 val () = printf "here's an int %d and a real %f.\n" 13 17.0
55 val () = printf "here's a real %f and an int %d.\n" 17.0 13
61 val printf: string -> int -> real -> unit
62 val printf: string -> real -> int -> unit
65 Again, this can't possibly working because SML doesn't have
66 overloading, and types can't depend on values.
69 == Idea: express type information in the format string ==
71 If we express type information in the format string, then different
72 uses of `printf` can have different types.
76 type 'a t (* the type of format strings *)
77 val printf: 'a t -> 'a
79 val fs1: (int -> real -> unit) t = "here's an int "D" and a real "F".\n"
80 val fs2: (int -> real -> real -> unit) t =
81 "here's three values ("D", "F", "F").\n"
82 val () = printf fs1 13 17.0
83 val () = printf fs2 13 17.0 19.0
86 Now, our two calls to `printf` type check, because the format
87 string specializes `printf` to the appropriate type.
90 == The types of format characters ==
92 What should the type of format characters `D` and `F` be? Each format
93 character requires an additional argument of the appropriate type to
94 be supplied to `printf`.
96 Idea: guess the final type that will be needed for `printf` the format
97 string and verify it with each format character.
101 type ('a, 'b) t (* 'a = rest of type to verify, 'b = final type *)
102 val ` : string -> ('a, 'a) t (* guess the type, which must be verified *)
103 val D: (int -> 'a, 'b) t * string -> ('a, 'b) t (* consume an int *)
104 val F: (real -> 'a, 'b) t * string -> ('a, 'b) t (* consume a real *)
105 val printf: (unit, 'a) t -> 'a
108 Don't worry. In the end, type inference will guess and verify for us.
111 == Understanding guess and verify ==
113 Now, let's build up a format string and a specialized `printf`.
118 val f0 = `"here's an int "
119 val f1 = f0 D " and a real "
124 These definitions yield the following types.
128 val f0: (int -> real -> unit, int -> real -> unit) t
129 val f1: (real -> unit, int -> real -> unit) t
130 val f2: (unit, int -> real -> unit) t
131 val p: int -> real -> unit
134 So, `p` is a specialized `printf` function. We could use it as
144 == Type checking this using a functor ==
151 val ` : string -> ('a, 'a) t
152 val D: (int -> 'a, 'b) t * string -> ('a, 'b) t
153 val F: (real -> 'a, 'b) t * string -> ('a, 'b) t
154 val printf: (unit, 'a) t -> 'a
157 functor Test (P: PRINTF) =
162 val () = printf (`"here's an int "D" and a real "F".\n") 13 17.0
163 val () = printf (`"here's three values ("D", "F ", "F").\n") 13 17.0 19.0
168 == Implementing `Printf` ==
170 Think of a format character as a formatter transformer. It takes the
171 formatter for the part of the format string before it and transforms
172 it into a new formatter that first does the left hand bit, then does
173 its bit, then continues on with the rest of the format string.
177 structure Printf: PRINTF =
179 datatype ('a, 'b) t = T of (unit -> 'a) -> 'b
181 fun printf (T f) = f (fn () => ())
183 fun ` s = T (fn a => (print s; a ()))
186 T (fn g => f (fn () => fn i =>
187 (print (Int.toString i); print s; g ())))
190 T (fn g => f (fn () => fn i =>
191 (print (Real.toString i); print s; g ())))
200 structure Z = Test (Printf)
204 == User-definable formats ==
206 The definition of the format characters is pretty much the same.
207 Within the `Printf` structure we can define a format character
212 val newFormat: ('a -> string) -> ('a -> 'b, 'c) t * string -> ('b, 'c) t =
213 fn toString => fn (T f, s) =>
214 T (fn th => f (fn () => fn a => (print (toString a); print s ; th ())))
215 val D = fn z => newFormat Int.toString z
216 val F = fn z => newFormat Real.toString z
220 == A core `Printf` ==
222 We can now have a very small `PRINTF` signature, and define all
223 the format strings externally to the core module.
230 val ` : string -> ('a, 'a) t
231 val newFormat: ('a -> string) -> ('a -> 'b, 'c) t * string -> ('b, 'c) t
232 val printf: (unit, 'a) t -> 'a
235 structure Printf: PRINTF =
237 datatype ('a, 'b) t = T of (unit -> 'a) -> 'b
239 fun printf (T f) = f (fn () => ())
241 fun ` s = T (fn a => (print s; a ()))
243 fun newFormat toString (T f, s) =
253 == Extending to fprintf ==
255 One can implement fprintf by threading the outstream through all the
263 val ` : string -> ('a, 'a) t
264 val fprintf: (unit, 'a) t * TextIO.outstream -> 'a
265 val newFormat: ('a -> string) -> ('a -> 'b, 'c) t * string -> ('b, 'c) t
266 val printf: (unit, 'a) t -> 'a
269 structure Printf: PRINTF =
271 type out = TextIO.outstream
272 val output = TextIO.output
274 datatype ('a, 'b) t = T of (out -> 'a) -> out -> 'b
276 fun fprintf (T f, out) = f (fn _ => ()) out
278 fun printf t = fprintf (t, TextIO.stdOut)
280 fun ` s = T (fn a => fn out => (output (out, s); a out))
282 fun newFormat toString (T f, s) =
285 (output (out, toString a)
294 * Lesson: instead of using dependent types for a function, express the
295 the dependency in the type of the argument.
297 * If `printf` is partially applied, it will do the printing then and
298 there. Perhaps this could be fixed with some kind of terminator.
300 A syntactic or argument terminator is not necessary. A formatter can
301 either be eager (as above) or lazy (as below). A lazy formatter
302 accumulates enough state to print the entire string. The simplest
303 lazy formatter concatenates the strings as they become available:
307 structure PrintfLazyConcat: PRINTF =
309 datatype ('a, 'b) t = T of (string -> 'a) -> string -> 'b
311 fun printf (T f) = f print ""
313 fun ` s = T (fn th => fn s' => th (s' ^ s))
315 fun newFormat toString (T f, s) =
318 th (s' ^ toString a ^ s)))
322 It is somewhat more efficient to accumulate the strings as a list:
326 structure PrintfLazyList: PRINTF =
328 datatype ('a, 'b) t = T of (string list -> 'a) -> string list -> 'b
330 fun printf (T f) = f (List.app print o List.rev) []
332 fun ` s = T (fn th => fn ss => th (s::ss))
334 fun newFormat toString (T f, s) =
337 th (s::toString a::ss)))
345 * <!Cite(Danvy98, Functional Unparsing)>