[Prev][Next][Index][Thread]
Re: Decidable polymorphic recursion?
Francois Pottier writes:
> I have had a quick look at your paper. I must be missing something
> obvious, but I fail to understand how it doesn't contradict
> Henglein's undecidability result. Henglein proves that
> semi-unification is reducible to typability in ML+FIX (i.e. given an
> expression, is there a valid typing judgement for it?). As far as as
> I understand, your paper claims:
>
> 1. typability in ML+FIX is equivalent to typability in ML'+FIX'.
> 2. typability in ML'+FIX' is decidable, since algorithm T0 computes principal
> typings.
>
> Taken together, these facts lead to a contradiction. What am I missing?
> I would very much like to understand where the subtlety lies.
Well... we believe that Henglein's proof [1] that semiunification is
reducible to type inference for ML+FIX has an incorrection, in theorem
3 (page 268), which states the equivalence of type systems MM' and
MM'' (defined in the paper). By rule (TAUT'') we can derive, for
example, A{x:a},a |- x:Int, since (a,a) <= (Int,a) (where (M1,M2) <=
(N1,N2) is defined in page 262, 1st paragraph). However A{x:a} |-
x:Int cannot be derived in MM'.
[1] F. Henglein, Type inference with polymorphic recursion,
ACM TOPLAS, 253--289, 15(2), 1993.