For Want of Difference Types

[winterkoninkje]

So I ran into a discussion on Lambda the Ultimate wherein was raised the topic of what the "real" mathematical type for (integral) division should be since :: Int -> Int -> Int doesn't cut it. Someone proposed :: Int -> Int -> Int+1, which is the normal way it's implemented— that is, the result is an integer or a singleton value representing (the single divide-by-zero) error it can generate. In a total functional world this has the problem of how to percolate exceptions up, since the caller isn't allowed to fail either.

That type is flagrantly wrong.

Invoking the abstract of the paper presented there (the site seems offline, so I can't read the paper), the reason it's flagrantly wrong is because it's not mathematical. Mathematics doesn't define an "undefined" value which would be permissible to return, it simply fails to define any value whatsoever. So if extending the result type is both mathematically incorrect and also a programming infrastructure nightmare, then what is the right answer?

The right answer is to restrict the inputs to the function. The usual way of doing this involves using dependent types to carry extra information about values in the types. Dependent types have many benefits (and many many issues), but we don't need even need them for this. All we need is difference types :: Int -> (Int \\ 0) -> Int.

In an ADT-based language like Haskell or ML, a type is a sum of products, for example the :: Maybe a type is either Nothing or Just a which can be expressed as 1+a. But in Haskell neither "Nothing" nor "Just a" are types, those names only exist in the data layer of the language, not the type layer. Sometimes we know for certain which branch of the type a value is in and I've often wanted to be able to treat the individual summands of a type as a type itself.[1]

Adding such an extension would not be too difficult, nor would it break the type inference algorithms in use, though it would require an, er, refinement of them[2]. In the underlying abstract machine of GHC, the case statement represents evaluation and hence is the only way to get the value from an expression. Case statements also give us proofs about which branch of a sum type a value resides in. That is, the following code is type correct.

> f :: Nothing -> b
> g :: Just a  -> b
>
> test :: Maybe a -> b
> test mx = case mx of
>           Nothing -> f mx
>           Just x  -> g mx
>
> -- This gives an identical proof
> test' mx@Nothing  = f mx
> test' mx@(Just x) = g mx

Coming into the test function we only know the maximal type that mx could have, and this is still inferable from looking at the heads of the case statement. But, once we've evaluated mx we have the proof necessary to refine the type to either :: Nothing or :: Just a. The type signatures of f and g are more restrictive, but we know that it is type safe to call them.

For the Maybe type this kind of refinement doesn't help very much because once we've refined things, the value is either unit (Nothing) or simply a (the Just tag gives us no additional information since Maybe contains exactly one extra bit of information and we already have that information from our proof). But for other types it can be quite helpful. Many of the standard list functions are not defined for empty lists and so being able to distinguish :: [] from :: (a : [a]) would be quite helpful in cleaning up the list library[3].

Similarly, being able to give compile-time proofs that an integer is not 0 lets us not only make many functions correct, but lets us do so without any run-time overhead for verifying this proof. In the same way, if we can give laws expressing the zeros and identities of functions, the compiler can use this information along with proofs that a particular value must be one of those special values in order to optimize the function call away all together. GHC already gives us some of that ability via rewrite rules, but the barrier to entry can be high and it would only work when the special value argument is a literal.

In addition to removing the errors thrown by basic library functions, difference types would enable us to do some more extreme hackery when it comes to coproduct types. The :: Either a b type is defined as Left a or Right b and is another frequent monad for error-prone functions (where a is the type of all possible errors, generally a string for simplicity). When dealing with this and other monads for capturing errors, we often find that the monad comes to take over the world, either because we need to propagate those errors or because we want a family of functions to return the same type for consistency's sake. In the latter case, declaring that a function returns Right b would allow the programmer to see uniform code, and let the compiler know that it can probably optimize the type tag away. Similarly, we often want to take an :: Either a b and convert it to an :: Either a c. As things stand, if we have a Left a we'll have to case match out the a and then rewrap it to obtain Left a. This extra work is unnecessary because the type Left a can freely and safely be cast up to forall b. Either a b; since the b doesn't exist in the value, it is free to be whatever is needed.

Having difference types would not make Haskell total. It would take full dependent types to restrict the inputs to the lookup function on maps and lists so that it's guaranteed to succeed. But having case-directed safe downcasting from a sum type to a refinement of that sum, and free upcasting from refined sums to less refined sums, would be really nice. And if we could write the :: Int -> (Int \\ 0) -> Int version of division, it would be easy to turn it into :: Int -> Int -> Maybe Int for the folks who like that sort of thing.

[1] The only way to do this in Haskell is to define each of the branches individually and then to define their union as another type. Doing this has many downsides including the double tagging of types, no free casting from the individual types to the union type, and not restricting the individual types to only being used in this particular union.

[2] Since a parameter's type may be narrowed in subexpressions rather than being constant in the whole function body.

[3] Note that the second argument to cons is still the full list type. The fixed point on types breaks things and allowing us to unroll the list's type further may lead to some of the problems encountered in dependent type systems. All I'm advocating here is that we have difference types as the strict inverse of union types so we can say :: ([a] \\ []) which is exactly :: (a : [a]).

Comments

[flexibeast.livejournal.com]

Difference types sound great; have there been arguments made against them? If so, what were those arguments?

[winterkoninkje.livejournal.com]

I'm not aware of any arguments against them, though I'm not aware of them being proposed before either. My knowledge of the dependent types literature is sparse, but from what I've seen, most of it is dashing headlong into full dependent types and trying to solve the problems that come with it. I've found considerably less on exploring the design space to say what pieces are tractable in isolation or where exactly it all starts to break down.

It's particularly funny that I came back to this old idea now and ranted about it, because the next day (last night) when working on the ICFP programming contest (http://www.icfpcontest.org/) I really wanted them so that I could implement the type for the incoming messages appropriately, i.e. as a union of record types (which GHC permits, but it isn't type-safe about the field accessors (i.e. you can call the accessors on any branch of the union, even if the other branches lack such a field)).

If I can get the free time to start hacking on GHC (ha!) or if I can convince my advisor that improving GHC will help for Dyna (ha! but maybe marginally less so) then I might see about implementing them myself and writing a couple papers on it. Right now types and type constructors are in a different namespace than functions and data constructors, with difference types we would still be making that distinction though how we discuss it needs to change[1] and how to reconcile that still needs to be worked out, along with some details about how they interact with the records syntax.


[1] Since the token Just could be either a type- or data-constructor now, depending on whether it's in a type context or an expression context.