[plt-scheme] Typed Scheme: type of filter ?

From: Michel Salim (michel.sylvan at gmail.com)
Date: Thu Jun 19 02:59:38 EDT 2008

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

In the POPL 08 paper, the type of filter is given as

(All (a b) ((a --b--> Boolean) (listof a) -> (Listof b))

which would allow one to do things like

(map add1 (filter number? '(1 #t 2 #f 3))

in fact, Sam gave this example on Lambda the Ultimate

In the released version of PLT Scheme 4.0, however, this is the type
of filter:
(All (a) ((<a> -> Boolean) (Listof <a>) -> (Listof <a>)))

which means the above failed. As can be verified:

(filter number? '(1 #t #f))
- - : (Listof (U Integer #f #t))
(1)

The handling of booleans also strikes me as a bit odd.

> > (define: bools : (Listof Boolean) '(#t #f))
> > bools
- - : (Listof Boolean)
(#t #f)
> > (define bools2 bools)
> > bools2
- - : (Listof Boolean)
(#t #f)
> > (define bools3 '(#t #f))
> > bools3
- - : (List #t #f)
(#t #f)

A similar behavior is exhibited for lists of numbers: '(1 1.5 2) :
(List Integer Number Integer), so heterogenous lists are treated just
like tuples in Haskell or ML, but is there any reason #t and #f are
not treated as just instances of Boolean ?

Thanks,

- --
Michel Salim
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.9 (GNU/Linux)
Comment: Using GnuPG with Fedora - http://enigmail.mozdev.org

iEYEARECAAYFAkhaA9kACgkQWt0J3fd+7ZDjrwCbBdDegJPsKbpD6P6eYsgq0h81
1BMAn2H5+gi5a+4UVnuLEp6AHJ37tL4B
=CTfP
-----END PGP SIGNATURE-----


Posted on the users mailing list.