Proving "no corruption" in Haskell

Question

I work in a safety-critical industry, and our software projects generally have safety requirements imposed; things that we have to demonstrate that the software does to a high degree of certainty. Often these are negatives, such as " shall not corrupt more frequently than 1 in ". (I should add that these requirements come from statistical system safety requirements).

One source of corruption is clearly coding errors, and I would like to use the Haskell type system to exclude at least some classes of these errors. Something like this:

First, here is our critical data item that must not be corrupted.

newtype Critical = Critical String 

Now I want to store this item in some other structures.

data Foo = Foo Integer Critical data Bar = Bar String Critical 

Now I want to write a conversion function from Foo to Bar which is guaranteed not to mess with the Critical data.

goodConvert, badConvert :: Foo -> Bar  goodConvert (Foo n c) = Bar (show n) c  badConvert (Foo n (Critical s)) = Bar (show n) (Critical $ "Bzzt - " ++ s) 

I want "goodConvert" to type check, but "badConvert" to fail type checking.

Obviously I can carefully not import the Critical constructor into the module that does conversion. But it would be much better if I could express this property in the type, because then I can compose up functions that are guaranteed to preserve this property.

I've tried adding phantom types and "forall" in various places, but that doesn't help.

One thing that would work would be to not export the Critical constructor, and then have

mkCritical :: String -> IO Critical 

Since the only place that these Critical data items get created is in the input functions, this makes some sense. But I'd prefer a more elegant and general solution.

Edit

In the comments FUZxxl suggested a look at Safe Haskell. This looks like the best solution. Rather than adding a "no corruption" modifier at the type level as I originally wanted, it looks like you can do it at the module level, like this:

1: Create a module "Critical" that exports all the features of the Critical data type, including its constructor. Mark this module as "unsafe" by putting "{-# LANGUAGE Unsafe #-}" in the header.

2: Create a module "SafeCritical" that re-exports everything except the constructor and any other functions that might be used to corrupt a critical value. Mark this module as "trustworthy".

3: Mark any modules that are required to handle Critical values without corruption as "safe". Then use this to demonstrate that any function imported as "safe" cannot cause corruption to a Critical value.

This will leave a smaller minority of code, such as input code that parses Critical values, requiring further verification. We can't eliminate this code, but reducing the amount that needs detailed verification is still a significant win.

The method is based on the fact that a function cannot invent a new value unless a function returns it. If a function only gets one Critical value (as in the "convert" function above) then that is the only one it can return.

A harder variation of the problem comes when a function has two or more Critical values of the same type; it has to guarantee not to mix them up. For instance,

swapFooBar :: (Foo, Bar) -> (Bar, Foo) swapFooBar (Foo n c1, Bar s c2) = (Bar s c1, Foo n c2) 

However this can be handled by giving the same treatment to the containing data structures.

Answer 1

You can use parametricity to get partway there

data Foo c = Foo Integer c data Bar c = Bar String c  goodConvert :: Foo c -> Bar c goodConvert (Foo n c) = Bar (show n) c 

Since c is an unconstrained type variable, you know that the function goodConvert cannot know anything about c, and therefore cannot construct a different value of that type. It has to use the one provided in the input.

Well, almost. Bottom values allow you to break this guarantee. However, you at least know that if you try to use a "corrupted" value, it will result in an exception (or non-termination).

badConvert :: Foo c -> Bar c badConvert (Foo n c) = Bar (show n) undefined