Implicit Parameters

[John Hughes]

	On Monday 04 February 2002 02:25 am, John Hughes wrote:
	> Not so fast! Proposing a "solution" means this is regarded as a "problem"!
	> But what is to say that the first behaviour is "right" in any general
	> sense?
	>
	> The important thing is that the language semantics is clear, and this is a
	> semantic question.  The static semantics of Haskell *is* clear: recursive
	> calls are monomorphic unless a type signature is given; this is the basis
	> for understanding the behaviour above. 

	I think part of the problem is that we've confused implicit parameterisation 
	with polymorphism.  Haskell has a two-level type system with monomorphic 
	types at the bottom level, and polymorphic and qualified types at the second 
	level.  It turned out to be very straightforward to add implicit parameters 
	to Haskell by treating them as a special kind of qualified type, and thus 
	they also play according to the rules of polymorphic types - i.e. you 
	`capture' implicit parameters exactly when you generalize a polymorphic 
	definition.

	However, Koen's example suggests that maybe implicit parameters shouldn't 
	necessarily play according to the rules of polymorphic types.  Perhaps 
	implciit parameters should be a special kind of monomorphic type instead.  If 
	this were the choice, then it's clear that they should be captured by 
	recursive definitions.

Yes, if one asks in isolation whether implicit parameters should belong at the
type level or the type scheme level, then it might seem reasonable to make
either choice. but bear in mind that the type/type scheme distinction is also
tied in with type inference. Namely, inferred types cannot contain nested type
schemes, only declared types may do so. (GHC's recent extension beyond rank 2
types doesn't change this basic fact).

If implicit parameters were to be moved to the type level, then it should also
be possible to infer types containing them in nested positions. For example,

         f x = (x with ?y = 1) + 1

should receive the inferred type

         f :: (Num a, Num b) => (?y :: a => b) -> b

What happens to principality? Even if there are principal types, can type
inference still be done fast (feels like inference in the presence of
subtypes)? These are hard questions!

I would be AGAINST moving implicit parameters to the type level, without
solving the inference problem satisfactorily. That would give Haskell three
sorts of types:

         inferrable types (no implicit parameters in nested positions)
	 declarable monomorphic types (nested implicit parameters)
	 type schemes

(And now, of course, one may wonder what kind of monomorphism the M-R refers
to...). Two sorts of types is, in my view, already enough.

John