[Haskell-cafe] Lack of expressiveness in kinds?

[Pablo Nogueira]

On 16/03/07, oleg at pobox.com <oleg at pobox.com> 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.