Hindley-Milner Inference Oddity w/ Twice Combinator
ajg opened this issue · 3 comments
It appears that the "twice" combinator is inferred by this h-m implementation as...
λf x. f (f x) :: ∀c d. (c → d) → c → d
...rather than the more common (e.g. GHCi)...
\f x -> f (f x) :: (t -> t) -> t -> t
-- or even:
\f -> f . f :: (b -> b) -> b -> b
...is this a known discrepancy/limitation?
I also noticed that applying one last substitution brings the former in line with the latter; i.e.:
λf x. f (f x) :: ∀d. (d → d) → d → d
One very simple way to achieve this lies in showType, by swapping...
case (runInfer . fmap (generalize (Env mempty) . snd) . infer env) expr of
...with...
case (runInfer . fmap (generalize (Env mempty) . uncurry applySubst) . infer env) expr of
...though I'm not sure whether that's correct in the general case. If it is, I'm happy to open a pull request for the change; the test suite seems happy with it.
You’re right, that inferred type is wrong. What’s the »one last substitution« you mention? Maybe I put that »snd« there because it’s type-correct, and then stopped thinking about whether it’s semantics-correct :-s
That was my thinking as well: it seems like the snd simply discards the substitutions rather than apply them. I opened #43 as one potential solution. Another option might be to offer a variant of infer that does this (or similar) internally and returns a plain MType rather than a (Subst, MType).
Merged the PR (thanks!). Can we close this issue?