[racket] Typed Racket: Parametricity foils equality checking?

On Thu, Nov 1, 2012 at 4:56 PM, John Clements <clements at brinckerhoff.org>
wrote:
> I can't tell whether this is a bug. In the program below,
remove-duplicates doesn't remove duplicates. This looks like an attempt to
preserve parametricity a la theorems for free, but I don't think that TR
actually tries to guarantee parametricity in this sense. I'm guessing that
the values in the list are being wrapped in contracts that prevent
'eq?'-checking; I thought that chaperones were supposed to... no, I
shouldn't even finish that sentence.

Typed Racket indeed doesn't guarantee parametricity for typed programs, but
the wrapping is necessary to preserve type soundness of typed programs.
Consider this program:

#lang typed/racket
(require/typed 'somewhere
[f (All (A) (A -> A))])

(: z : One)
(define z (add1 ((inst f Zero) 0)))

Since we can pick whatever type we want for a particular instantiation of
`f`, we have to make sure that no matter what sort of things we hand to
`f`, it gives only those sorts of things back. Since the contract has no
way to know which type you wanted, the only way it can ensure that the
"same sort of things" are produced is to make sure that they are actually
the same things.

This is implemented by wrapping the values, which additionally enforces
parametricity on the untyped code, but that isn't the goal.

Sam

>
> Anyhow, I'm just writing to make sure that this isn't a bug. It's
certainly not the behavior that I would naively expect. I can certainly
work around the bug by substituting a more specific type for
remove-duplicates, as in the commented-out version.
>
> John
>
> #lang typed/racket
>
> (require/typed racket
> [remove-duplicates (All (T) (Listof T) -> (Listof T))]
> #;[remove-duplicates ((Listof Symbol) -> (Listof Symbol))])
>
> (remove-duplicates '(a b c a d)) ;; => produces '(a b c a d)--that is, a
list with duplicates
>
>
> ____________________
> Racket Users list:
> http://lists.racket-lang.org/users
>

--
sam th
samth at ccs.neu.edu
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20121101/1de81b36/attachment.html>