I want to propose a modest extension to Haskell, which
would solve a common irritating problem in programming
in Haskell, and on-the-fly solves the practical programming
problems occuring due to the monomorphism restriction.


Problem Definition
==================

Currently, in Haskell, when defining functions, we can
either:

  a. specify no type at all, and it will be inferred;

  b. specify the complete type in all it's gory details.

The style of (b.) is commonly agreed upon to be a clear
style of programming, but there are some cases in which
it is not preferred:

  1. personal taste or just laziness (no pun intended).

  2. When the type (especially the context) gets
     very complicated.

When one does not want to program in style (b.), the
only option is to turn to style (a.).

This is unfortunate, because we still might want to
say *something* about the type, but just not the
whole context for example.

Moreover, in case (2.), we turn out to have a problem,
because the infamous monomorphism restriction kicks in;
sometimes we *have to* specify the type.

Here is an example:

  foo :: (Goggle a, Giggle b, Gaggle c) => a -> b -> c
  foo = goggleGiggleGaggle 42

When we decide that the type signature (read: context)
of "foo" is getting annoyingly large, we could simply
write:

  foo = goggleGiggleGaggle 42

Alas, the monomorphism restriction is complaining at
this point.

We have to tell the compiler "yes, I know this declaration
is not going to be shared", but in order to do so, have
to come up with it's complete type as well.


Practical Motivation
====================

I, and other people I have talked to recently, frequently
have to deal with this problem.

Especially in so-called "embedded domain-specific languages
with multiple interpretations" (Phew!), where you use a set
of overloaded combinators and a class hierarchy to distinguish
different properties of the various interpretations, one

  1. does not want to write down the complete types,
     because:

       a. the (inexperienced Haskell) programmer just
          uses the domain-specific language, and does
          not want to be bothered by Haskell types;

       b. the types can get very complicated due to
          heavy overloading.

  2. gets frequently bitten by the monomorphism
     restriction because of this, and because combinator-style
     programs usually have the form(*):

       composedObject = object1 <#> object2

  3. would really benefit from having *some* type information
     in the program, but often not all of it.

One example of such an embedded language is the hardware
description language Lava.


The Proposed Solution
=====================

We should allow "partial type specification". The programmer
is allowed to specify as much information about the type as
(s)he wants.

The partial type specification would be taken as a "skeleton",
merely filled in by the type inference algorithm.

Here is how we could specify partial type information
about foo:

  foo :: (..) => a -> b -> c

Or even:

  foo :: (Giggle a, ..) => a -> b -> c
  foo :: (Giggle a, Goggle b, ..) => a -> b -> c

(
Or we could maybe even use (..) at the *type* level:

  foo :: (..) => a -> (..) -> (..)
  foo :: (..) => (..)
)

So, we are allowed to use (..) at any place in the
context (or maybe even type), to show the compiler
that you know "something" should be there.


Difficulty of the Extension
===========================

The new extension does not pollute the syntax, I think,
because (..) is a special symbol already, but we were
not allowed to use it in the types.

I think it would be easy to extend most type check/inference
algorithms with this new feature. (Any comments on this?)

----

(*) the current solution in for example Lava is to write:

      composedObject () = object1 <#> object2

    because we did not want to bother students of the
    course "Hardware Description and Verification" with
    the anomalies of Haskell type classes.

    Instead, they could have written:

      composedObject :: (..) => sig Bool
      composedObject = object1 <#> object2

----

I would welcome any comments and suggestions (and proofs of
(un)soundness of formal definitions of the semantics :-)

Regards,
Koen.

--
Koen Claessen         http://www.cs.chalmers.se/~koen     
phone:+46-31-772 5424      e-mail:[EMAIL PROTECTED]
-----------------------------------------------------
Chalmers University of Technology, Gothenburg, Sweden

Reply via email to