[TYPES] Minimal type reconstruction

[Stefan Holdermans]

Hi all,

One way to look at type inference in Hindley-Milner-like disciplines  
is not just as the problem of finding a principal type scheme for a  
term in a given type environment, but as the problem of reconstructing  
an explicitly typed term in the style of System F that corresponds to  
such a principal type scheme. As an obvious example, consider the  
"completion" of the implicitly typed polymorphic identity function

	λx. x ,

resulting in the explicitly typed

	Λα. λx : α. x .

Typically, type inference for Hindley-Milner-like systems proceeds by  
assigning each let-bound variable its principal type. For example,  
completion of

	let id = λx. x in  id 2 + id 3 ni

yields

	let id = Λα. λx : α. x in id [ℕ] 2 + id [ℕ] 3 ni .

However, in this particular example the type abstraction in the  
definition of id and, hence, the type applications in the body of the  
local definition are unnecessary; another perfectly valid completion  
would be

	let id = λx : ℕ. x in id 2 + id 3 ni .

That is, if a let-bound variable is not used polymorphically, we may  
just as well infer a monomorphic type for it. In some specific  
situations, such a "minimal" completion may even be preferable over a  
fully polymorphic one. (Looking through a Curry-Howard lens, we are  
after the "simplest" proofs.) Although I'm quite sure it has been  
considered before, I have not found any discussion in literature of  
the problem of finding minimal completions. Can anyone on this list  
provide me with pointers to such discussions?

Thanks in advance,

	Stefan Holdermans