Home page > OCaml > Type fascism..

Type fascism..

Friday 26 August 2011, by Toots

I used to think of me as a libertarian.. Maybe it is because I am getting old and grumpy but I’ve found myself lately being more of a totalitarian rigid conservative.. concerning typing and APIs.. :-)

Liquidsoap being a stream-oriented software, we had felt the need for a long time to be able to manipulate mp3 id3 tags without them being attached to an actual file.. This is certainly possible in theory: id3 tags are not part of the mpeg I/II audio layer 3 format but an addition in the form of a binary blob, either at the beginning or at the end of the file. However, in practice there are very few libraries that actually support that — in fact there are very few implementations of the id3 tag specifications..

Anyway, I realize lately that, twisting TagLib’s arm, it was actually possible to implement this using this clean, maintained and well-designed library.. So I went on and upgraded our binding, adding what I called inline tags support. This allows to parse existing id3 binary tags or generate a binary representation of an inline tag that can be written to a file, or a stream in our case.

However, there are some constraints to consider in order to assure a proper use of the library, namely:

  • The user should be able to allocate empty inline tags.
  • An empty inline tag can be filled by parsing a binary blob representing an actual id3 tag
  • An can also be filled directly with id3 frames.
  • An initial empty inline tag is valid iff it has been filled with at least one frame or parsed from a valid id3 binary tag
  • Only valid inline tags should be rendered as binary blobs.

To make things more tricky, parsing a binary representation is done in two steps:

  • Parsing of the header, some initial 10 bytes. Only after this step is the total size of the binary data known.
  • Parsing of the full tag, using the size returned during header parsing.

And, of course, one should not do anything after parsing the header expect parsing the full tag, as the current state of the tag after parsing only the header is not consistent yet..

So, with all these considerations in mind, I wondered how it could be possible to restrict the freedom of the users while adding as few of a burden as possible, both for me and them.. As it turned out, phantom polymorphic types provide a very neat way of doing so!

Reading from above, an inline tag has 3 possible states:

type state = [`Invalid | `Parsed | `Valid]
  • `Invalid is the initial state of an empty tag
  • `Parsed is the state of a tag after parsing its header
  • `Valid is the state of a tag which is valid for rendering

Then, the full signature is as follows:

   type state = [ `Invalid | `Parsed | `Valid ]

   type 'a t

   val init : unit -> [`Invalid] t

   val header_size : int

   val parse_header : [`Invalid] t -> string -> [`Parsed] t

   val tag_size : [< `Parsed | `Valid] t -> int

   val parse_tag : [`Parsed] t -> string -> [`Valid] t

   val attach_frame : [< `Invalid | `Valid ] t -> frame_type -> frame_text -> [`Valid] t

   val render : [`Valid] t -> string

As you can see, the tag’s state is used as a phantom type in 'a t and is updated as the tag passes through the various API calls. This makes it impossible to actually hit render without either adding a single frame or successfully parsing a binary tag.

And it comes at zero cost, both for me and the user! As for myself, I just write the implementation bearing in mind that I need to return the given tag after each call. Likewise, the user only has to redefine its tag after each call, much like in the plain pure functional good ole fashion.. For instance:

let tag = init () in
let tag = attach_frame tag "TIT2" "The times They Are A-Changin'" in
render tag

I am too lazy to draw it but this can be generalized: if you think of your API as a diagram, where nodes represent states and arrows represent the various calls, then each state can be mapped to a polymorphic type and each call can be annotated with similar polymorphic phantom types in order to make sure that one can only call them from a correct state..

I think I really appreciate static typing when it comes at such a low cost. It makes you feel comfortable with both the code you write and the code people will write using your API and removes the need to constantly check boring things at runtime..

2 Forum messages

  • Type fascism.. Le 26 August 2011 à 17:36

    Pretty neat API! One question: You talked about the two-phase frame parsing: first the header, then (once you know its size) the actual data, but I don’t see this in the API. Did you elide it, is it up to the programmer, is there any way to avoid mistakes?

    Reply to this message

    • Type fascism.. Le 27 August 2011 à 01:34 , by Toots

      Indeed it is not.. It will actually raised an exception if the strings don’t have the right length..

      This is not an easy thing to do as this is a dynamic properly.. It could be possible to annotate the type of a parser header with the size of its parsed head.. But polymorphic types would not have enough expressivity as it would also need to check a type relation of the form: [`65] string => [`10] string..

      Reply to this message

Reply to this article