On 16/03/07, [EMAIL PROTECTED] [EMAIL PROTECTED] wrote:
There is a wide-spread opinion that one ought not to give context to a
data type declaration (please search for `restricted datatypes
Haskell'). Someone said that in GHC typechecker such contexts called
stupidctx. There has been a proposal to remove that feature from
Haskell, although I like it as a specification tool. John Hughes
wrote a paper about a better use for that feature:
I'd like to qualify this remark by adding that, to me, this opinion
arises from the fact that compilers treat constraints as orthogonal to
kinds, but not from the fact that constraints are a bad idea. I also
want to point Andrew to the fact that constraints are not associated
with the type but with (some of) the value constructors, perhaps in
order to keep the kind system intact. For example, define
data Eq a = Set a = MkSet [a]
I'd say we need the constraint in order to define a set. Nevertheless, evaluate
const 0 (undefined :: Set (Int - Int))
Funny we can give undefined the type Set (Int - Int) when functions
have no Eq instance.
Another example, define:
data Eq a = Foo a = FNil | FCons a (Foo a)
the type of the value constructors is :
FNil :: Foo a
FCons :: Eq a = a - Foo a - Foo a
By not putting the constraint in the polymorphic value FNil we may get
silly type errors when there are none.
As I understand, ideally the constraint restricts the range of types
to which the type constructor can be applied. Hardly a kind * - *
then, for * stands for the whole universe of types (not type
constructors). Passing the potato to the value system and letting the
value constructors bring up the constraints in construction or pattern
matching is not the same thing.
Then we have the complaint that if we want to use a constrained type
then we have to place constraints in all the functions that use it, so
why not put them there. In other words,
instead of
data Ord a = BinTree a = Leaf | Node a (BinTree a) (BinTree a)
insert :: Ord a = a - BinTree a - BinTree a
let's write:
data BinTree a = Leaf | Node a (BinTree a) (BinTree a)
insert :: Ord a = a - BinTree a - BinTree a
However, I find this wrong from a formal point of view. The constraint
is associated with the type, not the functions. Compare with the list
type and the function sort, which has an Ord constraint which belongs
to the function. There is no such thing as a constrained list *type*,
only that sort takes a list with elements in ord and no other list.
From a practical point of view,
if you like type inference, you may omit the constraint in the
functions if it appears in one place, that is, where the type is
defined. (To recall, John Hugues paper begins with the complaint that
changing the constraint in the type affects the type signatures of
functions when written explicitly.)
The solution perhaps is not to ignore constraints and treat them as a
minor evil, but to make them an integral part of the type system, as
entities that can be passed as arguments and returned as results at
the type level. And also as parameters to class declarations. A
questionable implementation decision should not be the origin of a
recommended style of programming.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
