Typed Racket: (set-member?) is unsound!

[tonyg]

Originally submitted on: Mon Mar 25 12:56:01 -0400 2013

The following program should be rejected by the type system, but is not, and runs, yielding #f.

Steps to Reproduce:

#lang typed/racket
(define x ((inst set String)))
(set-member? x 123)

Release:

5.3.3.7--2013-03-21(2f80cba8/d)

Environment:

unix "Linux stockholm.ccs.neu.edu 3.2.0-4-amd64 #1 SMP Debian 3.2.39-2 x86_64 GNU/Linux"
 (x86_64-linux/3m) (get-display-depth) = 32
Human Language: english
(current-memory-use) 410218308
Links: (links) = ("racl" "racket-typed-matrix" "racket-bitsyntax"); (links #:user? #f) =
 (); (links #:root? #t) = (#<path:/home/tonyg/src/racket-minecraft>); (links #:user? #f
 #:root? #t) = ()
Planet2 (show):
Installation-wide:
 [none]
User-specific, all-version:
 [none]
User-specific, version-specific (5.3.3.7):
 Package[*=auto]     Checksum    Source
 racket-minecraft    #f          (link /home/tonyg/src/racket-minecraft)

Collections:
("/home/tonyg/.racket/5.3.3.7/collects"
 ())
("/home/tonyg/src/racket/collects"
 ("slatex" "frtime" "test-engine" "unstable" "algol60" "texpict" "dynext" "db" "plai"
 "r6rs" "rackunit" "repo-time-stamp" "s-exp" "framework" "browser" "profile" "planet2"
 "setup" "scribble" "ffi" "handin-client" "slideshow" "parser-tools" "realm" "xrepl" "net"
 "reader" "sgl" "scheme" "scribblings" "typed-scheme" "hierlist" "readline" "math"
 "config" "raco" "deinprogramm" "teachpack" "swindle" "drscheme" "mred" "honu"
 "info-domain" "typed" "redex" "version" "file" "planet" "tests" "trace" "r5rs"
 ".gitignore" "racket" "mrlib" "2htdp" "compatibility" "eopl" "wxme" "lazy" "lang" "html"
 "srfi" "images" "racklog" "games" "errortrace" "scriblib" "launcher" "stepper"
 "preprocessor" "data" "at-exp" "mzcom" "meta" "htdp" "rnrs" "mzlib" "syntax-color"
 "compiler" "macro-debugger" "defaults" "picturing-programs" "schemeunit" "xml" "make"
 "mzscheme" "mysterx" "gui-debugger" "datalog" "drracket" "json" "icons" "typed-racket"
 "graphics" "help" "plot" "openssl" "syntax" "handin-server" "emb!
 edded-gui" "string-constants" "web-server" "future-visualizer"))

Computer Language: (("Determine language from source") (#(#t print mixed-fraction-e #f #t
 debug) (default) #() "#lang racket\n" #t #t ((main) (test))))

This bug was converted from Gnats bug 13629.

[endobson]

On Mon, 25 Mar 2013 10:09:15 -0700, eric.n.dobson at gmail dot com wrote:

What is unsound about it? Yes you can ask if a non string is in a (Setof String) and it will always return #f. If it had to be a string then you couldn't write this

(define x ((inst set String)))
(lambda: ((y : (U String Symbol)))
  (set-member? x y))

[tonyg]

On Mon, 25 Mar 2013 14:05:44 -0400, tonyg at ccs dot neu dot edu wrote:

On 03/25/2013 01:09 PM, Eric Dobson wrote:

What is unsound about it?

You're quite right, it's not unsound. (We've just had a long discussion here in the lab about this.) It is surprising to me though, and is a real usability issue, in that I had a (slightly more complex) instance of this in my program causing it to fail to terminate in production.

My bug was introduced in a refactoring, where I was relying on the type system to catch the type mismatches as if it were OCaml or Haskell. My understanding of TR was deficient and it led me into writing a bad program.

Sam intends to follow up with some thoughts on the issue.

Tony

[endobson]

On Thu, 25 Apr 2013 09:18:42 -0700, eric.n.dobson at gmail dot com wrote:

Sam: Do you have thoughts to share, or should I close this as WAI?

On Mon, Mar 25, 2013 at 11:05 AM, Tony Garnock-Jones tonyg@ccs.neu.edu wrote:

What is unsound about it? You're quite right, it's not unsound. (We've just had a long discussion here in the lab about this.) It is surprising to me though, and is a real usability issue, in that I had a (slightly more complex) instance of this in my program causing it to fail to terminate in production. My bug was introduced in a refactoring, where I was relying on the type system to catch the type mismatches as if it were OCaml or Haskell. My

[samth]

On Thu, 25 Apr 2013 12:22:01 -0400, samth at ccs dot neu dot edu wrote:

--001a11c1e2387be4af04db31d111 Content-Type: text/plain; charset=UTF-8

I'm trying to remember the thoughts I was going to put here. Tony, do you remember? On Apr 25, 2013 9:18 AM, "Eric Dobson" eric.n.dobson@gmail.com wrote:

On Mon, Mar 25, 2013 at 11:05 AM, Tony Garnock-Jones tonyg@ccs.neu.edu wrote:

What is unsound about it? You're quite right, it's not unsound. (We've just had a long discussion here in the lab about this.) It is surprising to me though, and is a real usability issue, in that I had a (slightly more complex) instance of this in my program causing it to fail to terminate in production. My bug was introduced in a refactoring, where I was relying on the type system to catch the type mismatches as if it were OCaml or Haskell. My understanding of TR was deficient and it led me into writing a bad program.

--001a11c1e2387be4af04db31d111 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

<p dir=3D"ltr">I'm trying to remember the thoughts I was going to put h= ere.=C2=A0 Tony, do you remember?

<div class=3D"gmail_quote">On Apr 25, 2013 9:18 AM, "Eric Dobson"= <<a href=3D"mailto:eric.n.dobson@gmail.com">eric.n.dobson@gmail.com= > wrote:<br type=3D"attribution"><blockquote class=3D"gmail_quote" style= =3D"margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> Sam: Do you have thoughts to share, or should I close this as WAI?

On Mon, Mar 25, 2013 at 11:05 AM, Tony Garnock-Jones <<a href=3D"mailto:= tonyg@ccs.neu.edu">tonyg@ccs.neu.edu> wrote:
> On 03/25/2013 01:09 PM, Eric Dobson wrote:
>>
>> What is unsound about it?
>
>
> You're quite right, it's not unsound. (We've just had a lo= ng discussion here
> in the lab about this.) It is surprising to me though, and is a real=
> usability issue, in that I had a (slightly more complex) instance of t= his in
> my program causing it to fail to terminate in production.
>
> My bug was introduced in a refactoring, where I was relying on the typ= e
> system to catch the type mismatches as if it were OCaml or Haskell. My=
> understanding of TR was deficient and it led me into writing a bad pro= gram.
>
> Sam intends to follow up with some thoughts on the issue.
>
> Tony