impredicative type checking

Jules Bean jules at jellybean.co.uk
Tue Nov 11 06:16:31 EST 2008


Jeff Polakow wrote:
> However, I don't see
> how they are not equivalent (in the presence of impredicative 
> polymorphism) since I can write
> derivations for both
> 
>     forall b. (b -> String /\ Int)  |-  (forall b. b -> String) /\ Int
> 
> and
> 
>     (forall b. b -> String) /\ Int  |-  forall b. (b -> String /\ Int)
> 
> in intuitionistic logic.

(Side-stepping your main point, rather, which I think Chris K answered 
correctly)

This is a non-sequitur.

The fact that A |- B and B |- A does not make them the same type. It 
makes them isomorphic types.

I can prove

(A \/ B) /\ C -| |- (A /\ C) \/ (B /\ C)

but that doesn't mean "(Either a b,c)" and "Either (a,c) (b,c)" are the 
same haskell type.

It does mean they are isomorphic types, neglecting bottoms.

But isomorphic types are not the same type, for the type checker!

Jules





More information about the Glasgow-haskell-users mailing list