[Haskell-cafe] Re: Type system speculation

Peter Verswyvelen bugfact at gmail.com
Fri Dec 11 12:15:16 EST 2009


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 <lrpalmer at gmail.com> wrote:
> 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
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>


More information about the Haskell-Cafe mailing list