[Haskell] intent-typing

[Tillmann Rendel]

Hi,

Marcus Sundman wrote:
> Hi, how would one go about implementing (or using if it's supported
> out-of-the-box) intent-typing* for haskell?

A basic technique is to use newtype declarations to declare separate 
types for separate intents.

   module StringSafety
            ( SafeString ()
            , UnsafeString ()
            , quote
            , considerUnsafe
            ) where

     newtype SafeString = SafeString String
     newtype UnsafeString = UnsafeString String

     considerUnsafe :: String -> UnsafeString
     considerUnsafe s = UnsafeString s

     quote :: UnsafeString -> SafeString
     quote (UnsafeString s) = SafeString s' where
       s' = ... s ...

This module does not export the SafeString and UnsafeString 
constructors, so we can be sure that no other code in the program can 
invent SafeStrings which are not really safe. Every string can be safely 
treated as unsafe, however, so we export a function considerUnsafe which 
does so.

Now, if we type our interface to the outside world as

   getInput      ::  ... -> UnsafeString
   sendOutput    ::  SafeString -> ...

we can be sure that a return value from getInput needs to pass through 
quote on its way to sendOutput, because quote is the only way to produce 
a SafeString.



This guarantuees safety. It has, however, a practical problem: We can't 
use the usual String functions on UnsafeString or SafeString values. For 
instance, we can't concatenate two UnsafeStrings using (++).

A naive solution would be to provide separate (++) functions for unsafe 
and safe strings:

   append_safe :: SafeString -> SafeString -> SafeString
   append_safe (SafeString x) (SafeString y)
     = SafeString (x ++ y)

   append_unsafe :: SafeString -> SafeString -> SafeString
   append_unsafe (UnsafeString x) (UnsafeString y)
     = UnsafeString (x ++ y)

Note that at least append_safe needs to be implemented in and exported 
from the StringSafety module. That is a good thing, because this 
function needs to be carefully checked for safety. The programmer needs 
to prove (or unit-test, or at least think about) the following theorem:

   If a and b are safe strings, so is a ++ b.

After this fact has been established, other modules are free to use 
append_safe however they like without possibly compromising safety.



Now, the above approach should work, but is still rather impractical: We 
need to copy the definitions of all String functions for unsafe and safe 
strings. However, since the bodies of all these copies are actually 
identical, so we can use parametric polymorphism to abstract over the 
difference between UnsafeString and SafeString. One way to achieve this 
is to use phantom types.

With phantom types, we declare only a single newtype for both safe and 
unsafe strings, but we annotate that type with an additional flag to 
distinguish safe from unsafe uses.

   module StringSafety
            ( AnnotatedString ()
            , Safe ()
            , Unsafe ()
            , quote
            , considerUnsafe
            , append
            ) where

     data Safe = Safe
     data Unsafe = Unsafe

     newtype AnnotatedString safety = AnnotatedString String

     considerUnsafe :: String -> AnnotatedString Unsafe
     considerUnsafe s = AnnotatedString s

     quote :: AnnotatedString Unsafe -> AnnotatedString Safe
     quote (AnnotatedString s) = AnnotatedString s' where
       s' = ... s ...

     append
       :: AnnotatedString a
       -> AnnotatedString a
       -> AnnotatedString a

     append (AnnotatedString x) (AnnotatedString y)
       = AnnotatedString (x ++ y)

Note that AnnotatedString does not really use its type parameter safety: 
That's why it is called a phantom type. The data constructor 
AnnotatedString can be freely used to convert between safe and unsafe 
strings, so we better not export it from the module. Inside the module, 
uses of the data constructor gives rise to proof obligations as above. 
So the programmer needs to reason that the following is true to justify 
the implementation and export of append:

   If x and y have the same safety level,
   then (x ++ y) has again that same safety level.

So now, we still have to write a wrapper around each string operation, 
but at least we need to write only one such wrapper for all intents, not 
a separate wrapper for each intent.


There is an inconvenience left: We can't concatenate safe and unsafe 
strings, because both arguments to append need to have exactly the same 
type. To fix this, we first have to figure out what the result of sucha 
concatenation would be: It would be an unsafe string, because at least 
one of the inputs is unsafe. We need to teach this kind of reasoning to 
the compiler, for instance, using type families:

   type family Join a b
   type instance Join Safe Safe = Safe
   type instance Join Safe Unsafe = Unsafe
   type instance Join Unsafe Safe = Unsafe
   type instance Join Unsafe Unsafe = Unsafe

The idea is that (Join a b) is the safety level of the result of an 
operation which consumes data of safety level a and b. I called the type 
family Join because the safety levels form a lattice, with unsafe levels 
higher then safe levels, and the type family computes the join operation 
for that lattice. So we are encoding a simple static analysis into the 
type system here!

Using this lattice structure of safety level, we can give a more 
polymorphic type to append:

   append
     :: AnnotatedString a
     -> AnnotatedString b
     -> AnnotatedString (Join a b)

The implementation can remain unchanged. Now, the programmer needs to 
reason that the following statement is true to justify this type of append:

   (x ++ y) is at least as safe as the least safe of x and y.



So to conclude, statically checked intent-typing can be expressed in 
Haskell using newtype wrappers with phantom types, and possibly some 
type-level computation on these phantom types to teach the compiler 
domain knowledge about the intents.

   Tillmann

PS. Crossposted to the haskell cafe, please consider dropping 
haskell at haskell.org when answering.