Re: [Haskell-cafe] Re: [Haskell] intent-typing
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. >
Re: [Haskell-cafe] Re: [Haskell] intent-typing
- Original Message > From: aditya siram > To: Haskell Café > Cc: hask...@haskell.org; Marcus Sundman > Sent: Tue, November 16, 2010 8:18:33 AM > Subject: Re: [Haskell-cafe] Re: [Haskell] intent-typing > > 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" ? The goal is to have ++ produce an AnnotatedString Safe or an AnnotatedString Unsafe, reflecting the safety level. A data family would maintain the distinction, but then AnnotatedString (Join Unsafe Unsafe) would not be equivalent to AnnotatedString Unsafe - and what if you want to concatenate three pieces? Brandon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: [Haskell] intent-typing
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 operati
[Haskell-cafe] Re: [Haskell] intent-typing
I still don't understand what intent typing is, but this particular problem is discussed (with a type-based, statically checked solution) at http://blog.moertel.com/articles/2006/10/18/a-type-based-solution-to-the-strings-problem --Max On Mon, Nov 15, 2010 at 17:17, Marcus Sundman wrote: > Hi, how would one go about implementing (or using if it's supported > out-of-the-box) intent-typing* for haskell? > > *) Intent-typing is compiler/verifier/parser enforced typing similar to > "apps hungarian" notation. E.g., say I have a webapp with fields for a > user's first name and last name, which I at some point show on another > webpage that the user loads, which is a typical XSS vulnerability situation. > So I have 2 functions, getParam(...) and setParam(...), which return the > value of a user-provided parameter and gives a parameter to the template > displayed to the user, respectively. I want to somehow flag the > getParam(...)-function as returning a user-provided string (say, > "unsafe-string"), and the setParam(...)-function as requiring a safely > encoded string (say, "safe-string"), so that if I sometimes forget to run > the user-provided string through some anti-xss-encoding thingy (which would > take an "unsafe-string" and return a "safe-string"), and don't (unit-)test > this particular aspect of said code, then some verifier thingy (preferably a > static verifier) would notice this and show me a warning. > > Cheers, > Marcus > ___ > Haskell mailing list > hask...@haskell.org > http://www.haskell.org/mailman/listinfo/haskell > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
