That was a great explanation of phantom types and type-families. I'm
just getting started on understand type families and I was wondering
why you didn't use data families in the truth table structure:
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
My understanding is that since 'type' just produces a type synonym and
the last three type instances are "Unsafe", they are equivalent.
Wouldn't it be better to have "data instance Join Safe Unsafe ..." so
that the compiler can distinguish between "Join Unsafe Safe", "Join
Safe Unsafe" and "Join Unsafe Unsafe" ?
-deech
2010/11/16 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@haskell.org when answering. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe