How are things like this handled in say - Morrow - using extensible records? I guess when one defines functions operating on extensible records you get a lot of reuse for free (in Andrew's example, you would just extend the record with either a Checked or Unchecked label) On Fri, Dec 11, 2009 at 12:02 AM, Luke Palmer wrote:

On Thu, Dec 10, 2009 at 1:46 PM, Andrew Coppin wrote:

...

oleg@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