[TYPES] Minimal type reconstruction

[Gavin Bierman]

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.9102

Gavin

-----Original Message-----
From: types-list-bounces at lists.seas.upenn.edu [mailto:types-list-bounces at lists.seas.upenn.edu] On Behalf Of Andrew Kennedy
Sent: 07 November 2008 15:07
To: 'Stefan Holdermans'; types-list at lists.seas.upenn.edu
Subject: Re: [TYPES] Minimal type reconstruction

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi Stefan

I think that

"Minimal Typing Derivations", N Bjorner, ACM Workshop on ML and its Applications, 1994

is probably what you're after. (Should be on citeseer but I don't seem to get access right now).

Cheers
Andrew.

-----Original Message-----
From: types-list-bounces at lists.seas.upenn.edu [mailto:types-list-bounces at lists.seas.upenn.edu] On Behalf Of Stefan Holdermans
Sent: 07 November 2008 08:24
To: types-list at lists.seas.upenn.edu
Subject: [TYPES] Minimal type reconstruction

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

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