[TYPES] Minimal type reconstruction

[Josef Svenningsson]

See:
 Minimal typing derivations
Nikolaj Skallerud Bjørner
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.9102

Josef

On Fri, Nov 7, 2008 at 9:24 AM, Stefan Holdermans <stefan at cs.uu.nl> wrote:
> [ 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