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