Re: monomorphic pattern binding

[Satish Thatte <satish@sun.mcs.clarkson.edu>]

Original-Via: uk.ac.nsf; Fri, 7 Sep 90 14:58:39 BST
Date: Fri, 7 Sep 90 09:11:41 EDT
From: Satish Thatte <satish@sun.mcs.clarkson.edu>
To: HASKLD-L <HASKLD-L%yalevm.bitnet@cs.yale.edu>,
        haskell <haskell%cs.yale.edu@clvm.clarkson.edu>
Subject: Re:  monomorphic pattern binding
Original-Sender: satish%edu.clarkson.mcs.sun%edu.clarkson.clvm%edu.yale.cs@yale.edu
Sender: haskell-request@cs.glasgow.ac.uk

I don't understand the question Amir and John raise about
soundness/completeness:

>  We are not so sure that the introduction
>  of monomorphism to Hindley Milner type system is sound or complete
>  in respect to HM soundness and completeness. This deserves a proof.

If the soundness and completeness of Haskell's type system have been
proved w.r.t.  Haskell's own typing rules (I haven't seen such a proof),
I don't see that the restrictive interpretation of bindings in the
pattern-binding law affects soundness and completeness.
Since Haskell's typing is really a translation, as they point out,
soundness only requires that the translated programs be well-typed.
Since monomorphism (I find this use of monomorphism disturbing --
I have always connected the word with quantfication, not overloading)
is a restriction which reduces the number of typable Haskell
programs without changing their translation, soundness is not
affected.  Completeness is usually considered a relation between
typing rules and a type assignment (or reconstruction) algorithm.
Again, if you make the typing *rules* more restrictive, I don't
see that this has an effect on completeness.

I should add that I share the misgivings of Amir and John about the
complexity of Haskell's type system.

Satish