[Haskell-cafe] Re: Type system speculation

[Luke Palmer]

On Thu, Dec 10, 2009 at 1:46 PM, Andrew Coppin
<andrewcoppin at btinternet.com> wrote:
> oleg at okmij.org wrote:
>>
>> Andrew Coppin wrote:
>>
>>>
>>> What we're really trying to do here is attach additional information to a
>>> value - information which exists only in the type checker's head, but has
>>> no
>>> effect on runtime behaviour.
>>>
>>
>> Haskell has had the ability to attach arbitrary many pieces of
>> (type-level) data to arbitrary types for a long time -- ever since
>> multi-parameter type classes and functional dependencies have been
>> introduced. Nowadays, type families accomplish the same with fewer
>> keystrokes. One merely needs to define a type family
>>        type family Attrib n index :: *
>> which maps the existing type n and the index to an arbitrary type.
>>
>
> Ah, good point. I hadn't thought of that!
>
> So it seems you can indeed attach arbitrary attributes to any type, any
> time. However, I don't immediately see a way to construct a "safe" string
> type and an "unsafe" string type, so that you can write code which
> distinguishes between them, but that existing code that just expects a plain
> ordinary string still works.

Well, what does existing code which just returns a plain ordinary
string return?  Presumably unsafe, so there would have to be a way to
bias.

> You could newtype string as two new types and
> attach whatever attributes you want to these types, but then normal string
> functions wouldn't work. Any ideas?

That is the way I do it, with explicit conversion functions to
indicate what I think is going on.  As I pointed out, while passing a
specialized version to ordinary functions might work (a common
technique in OO), getting them back is another matter.

module SafeString (String, fromSafe, safe)
import Prelude hiding (String)

newtype String = String { fromSafe :: Prelude.String }

safe :: Prelude.String -> Maybe String
safe s | verify s = Just (String s)
       | otherwise = Nothing

And put in calls to safe and fromSafe explicitly.  You might see this
as a pain, but half of them (the safe calls) are adding value by
forcing you to deal with it if your transformations are not
safety-preserving.  The fromSafe calls could technically be omitted,
though you could argue that they are providing a nice abstraction
barrier too:  SafeStrings, being a subtype, might have a better
representation[1] than ordinary Strings, which you may later decide,
so fromSafe is providing you with the opportunity to change that later
without affecting the client code.

[1] For example (1) a bit-packed representation to save a little
space, or (2) allowing the SafeString module to be reproduced in a
proof assistant where the String type contains proof of its safety, so
that you can verify the client code verbatim  (This is currently not
possible, but it is something I imagine being possible :-).

Luke