F# and statically checked union cases

Question

Soon me and my brother-in-arms Joel will release version 0.9 of Wing Beats. It's an internal DSL written in F#. With it you can generate XHTML. One of the sources of inspiration have been the XHTML.M module of the Ocsigen framework. I'm not used to the OCaml syntax, but I do understand XHTML.M somehow statically check if attributes and children of an element are of valid types.

We have not been able to statically check the same thing in F#, and now I wonder if someone have any idea of how to do it?

My first naive approach was to represent each element type in XHTML as a union case. But unfortunately you cannot statically restrict which cases are valid as parameter values, as in XHTML.M.

Then I tried to use interfaces (each element type implements an interface for each valid parent) and type constraints, but I didn't manage to make it work without the use of explicit casting in a way that made the solution cumbersome to use. And it didn't feel like an elegant solution anyway.

Today I've been looking at Code Contracts, but it seems to be incompatible with F# Interactive. When I hit alt + enter it freezes.

Just to make my question clearer. Here is a super simple artificial example of the same problem:

type Letter = 
    | Vowel of string
    | Consonant of string
let writeVowel = 
    function | Vowel str -> sprintf "%s is a vowel" str

I want writeVowel to only accept Vowels statically, and not as above, check it at runtime.

How can we accomplish this? Does anyone have any idea? There must be a clever way of doing it. If not with union cases, maybe with interfaces? I've struggled with this, but am trapped in the box and can't think outside of it.

Answer 1

It looks like that library uses O'Caml's polymorphic variants, which aren't available in F#. Unfortunately, I don't know of a faithful way to encode them in F#, either.

One possibility might be to use "phantom types", although I suspect that this could become unwieldy given the number of different categories of content you're dealing with. Here's how you could handle your vowel example:

module Letters = begin
  (* type level versions of true and false *)
  type ok = class end
  type nok = class end

  type letter<'isVowel,'isConsonant> = private Letter of char

  let vowel v : letter<ok,nok> = Letter v
  let consonant c : letter<nok,ok> = Letter c
  let y : letter<ok,ok> = Letter 'y'

  let writeVowel (Letter(l):letter<ok,_>) = sprintf "%c is a vowel" l
  let writeConsonant (Letter(l):letter<_,ok>) = sprintf "%c is a consonant" l
end

open Letters
let a = vowel 'a'
let b = consonant 'b'
let y = y

writeVowel a
//writeVowel b
writeVowel y

Answer 2

Strictly speaking, if you want to distinguish between something at compile-time, you need to give it different types. In your example, you could define two types of letters and then the type Letter would be either the first one or the second one.

This is a bit cumbersome, but it's probably the only direct way to achieve what you want:

type Vowel = Vowel of string
type Consonant = Consonant of string
type Letter = Choice<Vowel, Consonant>

let writeVowel (Vowel str) = sprintf "%s is a vowel" str
writeVowel (Vowel "a") // ok
writeVowel (Consonant "a") // doesn't compile

let writeLetter = function
  | Choice1Of2(Vowel str) -> sprintf "%s is a vowel" str
  | Choice2Of2(Consonant str) -> sprintf "%s is a consonant" str

The Choice type is a simple discriminated union which can store either a value of the first type or a value of the second type - you could define your own discriminated union, but it is a bit difficult to come up with reasonable names for the union cases (due to the nesting).

Code Contracts allow you to specify properties based on values, which would be more appropriate in this case. I think they should work with F# (when creating F# application), but I don't have any experience with integrating them with F#.

For numeric types, you can also use units of measure, which allow you to add additional information to the type (e.g. that a number has a type float<kilometer>), but this isn't available for string. If it was, you could define units of measure vowel and consonant and write string<vowel> and string<consonant>, but units of measure focus mainly on numerical applications.

So, perhaps the best option is to rely on runtime-checks in some cases.

[EDIT] To add some details regarding the OCaml implementation - I think that the trick that makes this possible in OCaml is that it uses structural subtyping, which means (translated to the F# terms) that you can define discriminated union with some mebers (e.g. only Vowel) and then another with more members (Vowel and Consonant).

When you create a value Vowel "a", it can be used as an argument to functions taking either of the types, but a value Consonant "a" can be used only with functions taking the second type.

This unfrotunately cannot be easily added to F#, because .NET doesn't natively support structural subtyping (although it may be possible using some tricks in .NET 4.0, but that would have to be done by the compiler). So, I know understand your problem, but I don't have any good idea how to solve it.

Some form of structural subtyping can be done using static member constraints in F#, but since discriminated union cases aren't types from the F# point of view, I don't think it is usable here.

Answer 3

My humble suggestion is: if the type system does not easily support statically checking 'X', then don't go through ridiculous contortions trying to statically check 'X'. Just throw an exception at runtime. The sky will not fall, the world will not end.

Ridiculous contortions to gain static checking often come at the expense of complicating an API, and make error messages indecipherable, and cause other degradations at the seams.