[mercury-users] typeclass constraint on type definition... wrong

[Richard A. O'Keefe]

David Jeffery wrote:

	This is a little bit of extra typing, but we decided not to go with the
	syntax you were trying to use because we didn't want to commit ourselves to
	supporting something that we were not sure was a good idea (after all, it
	really is just shorthand).
	
No, it is *NOT* just shorthand.
As it happens, I'm teaching a functional programming class using Haskell.
Their second assignment was to find a priority queue implementation they
liked (I gave them a list of about a dozen and said that others would be
allowed), code it up in Haskell, and get it going.

Now, for a priority queue, you really *really* want this:

    Ord k => data PQ k v = <whatever>

    new_pq   :: PQ k v
    add_pq   :: PQ k v -> k -> v -> PQ k v
    empty_pq :: PQ k v -> Bool
    remin_pq :: PQ k v -> ((k,v), PQ k v)
    merge_pq :: PQ k v -> PQ k v -> PQ k v

The constraint that k belong to the Ord type class is not
an "accidental" property of some of the *functions*, it's
a fundamental property of the priority queue *type*.

Mercury is supposed to be logic programming language that can be
offered to software engineers with a straight face.  Forcing
crucial information to be ripped out of the type declaration
and replicated perhaps dozens of times in the functions of the
type is *not* good software engineering.  Ada and Eiffel, for
example, would *definitely* put that constraint as a constraint
on the generic parameters of the package/class, *not* as a
constraint on the operations of the type.

The new_pq function (which makes empty priority queues)
and the empty_pq function (which recognises empty priority queues)
almost certainly make no use of the ordering property of the keys,
because in the cases they care about there *are* no keys to compare.
So it is quite typical to find people writing

    data PQ k v = <whatever>

    new_pq   ::          PQ k v
    add_pq   :: Ord k => PQ k v -> k -> v -> PQ k v
    empty_pq ::          PQ k v -> Bool
    remin_pq :: Ord k => PQ k v -> ((k,v), PQ k v)
    merge_pq :: Ord k => PQ k v -> PQ k v -> PQ k v

perhaps because they start by writing functions with no types,
and then copy the types the compiler infers.

But this is *wrong*.  It allows you to write

    impossible :: PQ (Int -> Int -> Int) Int
    impossible = new_pq

which will get through the type checker, but which is not in fact
a meaningful priority queue.  This kind of mistake is easy to make:
I've just swapped the key and value arguments.  To be sure, if
'impossible' is used, a type error will be reported further down
the track.  But it *ought* to be reported *here*.

It also means that in Haskell certain things don't get inferred
and have to be stated by the programmer, because the information
that the type parameters must be constrained is not available at
the point where it's needed.

--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------