<p dir="ltr"></p>
<p dir="ltr">On Thu, Nov 1, 2012 at 4:56 PM, John Clements <<a href="mailto:clements@brinckerhoff.org">clements@brinckerhoff.org</a>> wrote:<br>
> 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.</p>
<p dir="ltr">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:</p>
<p dir="ltr">#lang typed/racket<br>
(require/typed 'somewhere<br>
[f (All (A) (A -> A))])</p>
<p dir="ltr">(: z : One)<br>
(define z (add1 ((inst f Zero) 0)))</p>
<p dir="ltr">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.</p>
<p dir="ltr">This is implemented by wrapping the values, which additionally enforces parametricity on the untyped code, but that isn't the goal.</p>
<p dir="ltr"> Sam</p>
<p dir="ltr">><br>
> 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.<br>
><br>
> John<br>
><br>
> #lang typed/racket<br>
><br>
> (require/typed racket<br>
> [remove-duplicates (All (T) (Listof T) -> (Listof T))]<br>
> #;[remove-duplicates ((Listof Symbol) -> (Listof Symbol))])<br>
><br>
> (remove-duplicates '(a b c a d)) ;; => produces '(a b c a d)--that is, a list with duplicates<br>
><br>
><br>
> ____________________<br>
> Racket Users list:<br>
> <a href="http://lists.racket-lang.org/users">http://lists.racket-lang.org/users</a><br>
><br><br></p>
<p dir="ltr">--<br>
sam th<br>
<a href="mailto:samth@ccs.neu.edu">samth@ccs.neu.edu</a></p>