Rank-2 polymorphism & type inference

[Carlos Camarao de Figueiredo]

--udgwjrnSq1
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7bit


Hello.

<  class C t where op :: t -> Bool
<  instance C [t] where op x = True
<
<  p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ [])
<  q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f)
<
<The definitions of p and q differ only in the order of the components in
<the pair on their right-hand sides.  And yet:
<
<  ghc and "Typing Haskell in Haskell" reject p, but accept q;
<  Hugs rejects q, but accepts p;
<  hbc rejects both p and q;
<  nhc98 ... (Malcolm, can you fill in the blank for us!).

System CT accepts both. No type signature is required.

The types inferred for p and q are, resp.:

  Forall a,b. [a] -> (b -> Bool, [a])  and
  Forall a,b. [a] -> ([a], b -> Bool) 
 
You can run the attached "encoded" program (in which 'op' is
overloaded, instead of having its type annotated in a type class) in
CTinH (http://www.dcc.ufmg.br/~camarao/CT/CTinH.tar.gz). Type
inference in system CT is explained in a paper available at
http://www.dcc.ufmg.br/~camarao/CT/CT.ps.gz (see also homepage at
http://www.dcc.ufmg.br/~camarao/CT).

Carlos


--udgwjrnSq1
Content-Type: application/octet-stream
Content-Disposition: attachment;
	filename="l.hs"
Content-Transfer-Encoding: base64

bW9kdWxlIFNvdXJjZVByZWx1ZGUgd2hlcmUKCmltcG9ydCBUZXN0YmVkCmltcG9ydCBIYXNr
ZWxsUHJpbXMKaW1wb3J0IFN0ZFByZWwKCi0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tCi0tIFRl
c3QgRnJhbWV3b3JrOgoKbWFpbiA6OiBJTyAoKQptYWluICA9IHRlc3QgZGVmbnNIYXNrZWxs
UHJpbXMgcHJlbHVkZURlZm5zCgpzYXZlUHJlbHVkZSA6OiBJTyAoKQpzYXZlUHJlbHVkZSAg
PSBzYXZlICJ4Lm91dCIgZGVmbnNIYXNrZWxsUHJpbXMgcHJlbHVkZURlZm5zCgotLS0tLS0t
LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
LS0tLS0tLS0tLS0tLS0tLQotLSBNYWluIGRlZmluaXRpb25zOgoKcHJlbHVkZURlZm5zIDo6
IFtCaW5kR3JvdXBdCnByZWx1ZGVEZWZucwogPSBtYXAgdG9CZwogICBbCi0tIGluc3RhbmNl
IEMgW3RdIHdoZXJlIG9wIHggPSBUcnVlCiAgICBbKCJvcCIsTm90aGluZywgWyhbcE5pbF0s
IGVjb25zdCB0cnVlQyldKV0sIAoKLS0gaW5zdGFuY2UgQyBbdF0gd2hlcmUgb3AgeCA9IFRy
dWUKICAgIFsoIm9wIixOb3RoaW5nLCBbKFtQQ29uIHRydWVDIFtdXSwgZWNvbnN0IHRydWVD
KV0pXSwgCgotLSBwIHkgPSAobGV0IGYgOjogYyAtPiBCb29sCi0tICAgICAgICAgICAgZiB4
ID0gb3AgKHkgPj4gcmV0dXJuIHgpCi0tICAgICAgICBpbiBmLCB5ICsrIFtdKQogICAgWygi
cCIsTm90aGluZywgCiAgICAgIFsoW1BWYXIgInkiXSwgYXAgW2Vjb25zdCB0dXAyQywgCiAg
ICAgICAgICAgICAgICAgICAgICAgIGVsZXQgW1soImYiLCBKdXN0IChGb3JhbGwgKFtdIDo9
PiAoVEdlbiAwIGBmbmAgdEJvb2wpKSksIAogICAgICAgICAgICAgICAgICAgICAgICAgICAg
ICAgICAgWyhbUFZhciAieCJdLCBhcCBbZXZhciAib3AiLCAKICAgICAgICAgICAgICAgICAg
ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICBhcCBbZWNvbnN0IHRoZW5NLCBldmFy
ICJ5IiwgCiAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg
ICAgICAgYXAgW2Vjb25zdCByZXR1cm5NLCAoZXZhciAieCIpXV1dKV0pXV0KICAgICAgICAg
ICAgICAgICAgICAgICAgICAgICAgKGV2YXIgImYiKSwgIGFwIFtldmFyICIrKyIsIGV2YXIg
InkiLCBlTmlsXV0pXSldLAotLSBxIHkgPSAoeSArKyBbXSwgCi0tICAgICAgICAgIGxldCBm
IDo6IGMgLT4gQm9vbAotLSAgICAgICAgICAgIGYgeCA9IG9wICh5ID4+IHJldHVybiB4KQot
LSAgICAgICAgaW4gZikKICAgIFsoInEiLE5vdGhpbmcsIAogICAgICBbKFtQVmFyICJ5Il0s
IGFwIFtlY29uc3QgdHVwMkMsIAogICAgICAgICAgICAgICAgICAgICAgICBhcCBbZXZhciAi
KysiLCBldmFyICJ5IiwgZU5pbF0sCiAgICAgICAgICAgICAgICAgICAgICAgIGVsZXQgW1so
ImYiLCBKdXN0IChGb3JhbGwgKFtdIDo9PiAoVEdlbiAwIGBmbmAgdEJvb2wpKSksIAogICAg
ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgWyhbUFZhciAieCJdLCBhcCBbZXZhciAi
b3AiLCAKICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg
ICBhcCBbZWNvbnN0IHRoZW5NLCBldmFyICJ5IiwgCiAgICAgICAgICAgICAgICAgICAgICAg
ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgYXAgW2Vjb25zdCByZXR1cm5NLCAoZXZh
ciAieCIpXV1dKV0pXV0KICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgKGV2YXIgImYi
KV0pXSldLAogICAgWygiKysiLAogICAgICBKdXN0IChGb3JhbGwgCiAgICAgICAgICAgICAo
W10gOj0+IAogICAgICAgICAgICAgIChUQXAgdExpc3QgKFRHZW4gMCkgYGZuYCBUQXAgdExp
c3QgKFRHZW4gMCkgYGZuYCBUQXAgdExpc3QgKFRHZW4gMCkpKSksCiAgICAgIFsoW3BOaWws
IFBWYXIgInlzIl0sCiAgICAgICAgZXZhciAieXMiKSwKICAgICAgIChbUENvbiBjb25zQyBb
UFZhciAieCIsIFBWYXIgInhzIl0sIFBWYXIgInlzIl0sCiAgICAgICAgYXAgW2Vjb25zdCBj
b25zQywgZXZhciAieCIsIGFwIFtldmFyICIrKyIsIGV2YXIgInhzIiwgZXZhciAieXMiXV0p
XSldCiAgIF0KCg==

--udgwjrnSq1
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7bit





--udgwjrnSq1--