Ensuring consistency in typeclass instances?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Ensuring consistency in typeclass instances?

Colin Paul Adams
Hello,

I'm just reading through Real World Haskell - chapter 6 (typeclasses).

The definition of Eq is shown, and it mentions that you can define
either one or both of the two classes.

What would happen if I were two define both == and /= for an instance,
in such a way that they were not opposites?

If I were doing this in Eiffel, the function definitions would have
postconditions to state the relationships, and the first execution
would trigger a violation, telling me what was wrong. Is there any
similar facility in Haskell?
--
Colin Adams
Preston Lancashire
Reply | Threaded
Open this post in threaded view
|

Ensuring consistency in typeclass instances?

Brent Yorgey-2
On Tue, Nov 25, 2008 at 05:52:06PM +0000, Colin Paul Adams wrote:

> Hello,
>
> I'm just reading through Real World Haskell - chapter 6 (typeclasses).
>
> The definition of Eq is shown, and it mentions that you can define
> either one or both of the two classes.
>
> What would happen if I were two define both == and /= for an instance,
> in such a way that they were not opposites?
>
> If I were doing this in Eiffel, the function definitions would have
> postconditions to state the relationships, and the first execution
> would trigger a violation, telling me what was wrong. Is there any
> similar facility in Haskell?

Nope.  You will just get (possibly) inconsistent results.  There are
many other typeclasses like this as well (Functor, Monoid, Monad...)
where the methods are supposed to satisfy certain laws about how they
relate to one another, but Haskell has no way to guarantee this.

A meta-level point is that Haskell (and strongly-typed languages in
general) are all about *static* (compile-time) verification.  Having a
program which dynamically (at run-time) checks that certain properties
hold, a la Eiffel, is generally a rather un-Haskellish way of doing
things.  As much as possible, I would like to know for sure that if my
Haskell program compiles, it will not exhibit any run-time errors.

So, to check constraints statically rather than dynamically, they must
be put in the type system.  But the sorts of constraints you're asking
about (type class laws) often need dependent types (which Haskell
doesn't have) to be expressed elegantly.

-Brent
Reply | Threaded
Open this post in threaded view
|

Ensuring consistency in typeclass instances?

Colin Paul Adams
>>>>> "Brent" == Brent Yorgey <[hidden email]> writes:

    Brent> On Tue, Nov 25, 2008 at 05:52:06PM +0000, Colin Paul Adams wrote:
    >> Hello,
    >>
    >> I'm just reading through Real World Haskell - chapter 6
    >> (typeclasses).
    >>
    >> The definition of Eq is shown, and it mentions that you can
    >> define either one or both of the two classes.
    >>
    >> What would happen if I were two define both == and /= for an
    >> instance, in such a way that they were not opposites?
    >>
    >> If I were doing this in Eiffel, the function definitions would
    >> have postconditions to state the relationships, and the first
    >> execution would trigger a violation, telling me what was
    >> wrong. Is there any similar facility in Haskell?

    Brent> Nope.  You will just get (possibly) inconsistent results.
    Brent> There are many other typeclasses like this as well
    Brent> (Functor, Monoid, Monad...)  where the methods are supposed
    Brent> to satisfy certain laws about how they relate to one
    Brent> another, but Haskell has no way to guarantee this.

    Brent> A meta-level point is that Haskell (and strongly-typed
    Brent> languages in general) are all about *static* (compile-time)
    Brent> verification.  Having a program which dynamically (at
    Brent> run-time) checks that certain properties hold, a la Eiffel,
    Brent> is generally a rather un-Haskellish way of doing things.

I don't see why. Eiffel is strongly typed too. But current compiler
technology doesn't necessarily permit us to check all we would like
statically (as you say below).

It seems to me, having read further, that QuickCheck does just this
(and is an answer to my own original question).
But so far I'm only reading. I guess when I try it out I might find
out different.
 
    Brent> So, to check constraints statically rather than
    Brent> dynamically, they must be put in the type system.  But the
    Brent> sorts of constraints you're asking about (type class laws)
    Brent> often need dependent types (which Haskell doesn't have) to
    Brent> be expressed elegantly.
--
Colin Adams
Preston Lancashire
Reply | Threaded
Open this post in threaded view
|

Ensuring consistency in typeclass instances?

Brent Yorgey-2
On Wed, Nov 26, 2008 at 05:04:52PM +0000, Colin Paul Adams wrote:
> >>>>> "Brent" == Brent Yorgey <[hidden email]> writes:
>
> I don't see why. Eiffel is strongly typed too. But current compiler
> technology doesn't necessarily permit us to check all we would like
> statically (as you say below).
>
> It seems to me, having read further, that QuickCheck does just this
> (and is an answer to my own original question).

True, I should have mentioned QuickCheck in my previous email.  It's
not *quite* the same thing -- in particular, it tests properties you
specify on randomly generated values, rather than testing the actual
values which occur at runtime.  But in many cases that's just as good,
and has the additional benefit that it separates the property testing
from execution -- so you can have confidence in certain semantic
properties without the possibility of run-time exceptions.

-Brent