On Thu, Dec 10, 2009 at 1:46 PM, Andrew Coppin
<andrewcop...@btinternet.com> wrote:
> o...@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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
