This happens because xs and ys don't actually have the same type. The REPL in TR provides the information:
> xs - : (Listof 'a) [more precisely: (List 'a 'a)] '(a a) > ys - : (Listof 'a) '(a a) It's that "more precisely" bit that's crucial. TR knowns that xs has exactly two elements, but it doesn't know that about `ys` (because it doesn't have fancy types for `make-list`, and in fact can't expresses them even if we wanted to). Sam On Sat, Jan 24, 2015 at 8:15 PM, Matthew Butterick <m...@mbtype.com> wrote: > Thank you for the tip. I'm afraid I'm still unclear why this happens, > however: > > #lang typed/racket > (: mb-hash : (All (A B) (Rec lst (U Null (List* A B lst))) -> (HashTable A > B))) > (define (mb-hash xs) > (let loop ([hsh : (HashTable A B) (hash)] [xs : (Rec lst (U Null (List* A > B lst))) xs]) > (match xs > [(list) hsh] > [(list-rest a b rst) (loop (hash-set hsh a b) rst)]))) > > (define xs '(a a)) > (define ys (make-list 2 'a)) > > xs ; (Listof 'a) > ys ; (Listof 'a) > > (mb-hash xs) ; typecheck succeeds > (mb-hash ys) ; typecheck fails > > > > > > On Sat, Jan 24, 2015 at 1:10 PM, Alexander D. Knauth <alexan...@knauth.org> > wrote: >> >> For something like that, this works, and supports polymorphism, checks an >> even number of elements, and separates the key types from the value types: >> #lang typed/racket >> (: mb-hash : (All (A B) (Rec lst (U Null (List* A B lst))) -> (HashTable A >> B))) >> (define (mb-hash xs) >> (let loop ([hsh : (HashTable A B) (hash)] [xs : (Rec lst (U Null (List* >> A B lst))) xs]) >> (match xs >> [(list) hsh] >> [(list-rest a b rst) (loop (hash-set hsh a b) rst)]))) >> (define xs '(width 10 foo bar zam 42)) >> (mb-hash xs) >> ;'#hash((width . 10) (foo . bar) (zam . 42)) >> >> Before the repo was split, there was a pull request by Asumu Takikawa >> here: >> https://github.com/plt/racket/pull/564 >> which would allow something like this to be used for a type for hash, >> where the arguments wouldn’t have to be in a list like this. >> >> On Jan 24, 2015, at 2:50 PM, Matthew Butterick <m...@mbtype.com> wrote: >> >>> For this issue, Alex just submitted a patch, so it will be fixed soon. >>> >>> In general, TR doesn't work well with functions like `hash` that take >>> their arguments in pairs or triples, and thus they end up having >>> simpler types than the full Racket behavior. >> >> >> >> In my case, I've already committed to indefinite-arity `hash` as part of >> the program interface (a decision I could reconsider, though it would >> require a new quantum of benefit to be worthwhile) >> >> Am I wrong that this TR function approximates the standard `hash` (by >> unpacking the arguments manually)? >> >> If not, is this approach disfavored for some other reason? >> >> ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; >> #lang typed/racket/base >> >> (: mb-hash ((Listof Any) . -> . HashTableTop)) >> (define (mb-hash xs) >> (let-values ([(ks vs even?) (for/fold >> ([ks : (Listof Any) null][vs : (Listof Any) >> null][even? : Boolean #t]) >> ([x (in-list xs)]) >> (if even? >> (values (cons x ks) vs #f) >> (values ks (cons x vs) #t)))]) >> (when (not even?) (error 'bad-input)) >> (for/hash ([k (in-list ks)][v (in-list vs)]) >> (values k v)))) >> >> (define xs '(width 10 foo bar zam 42)) >> (mb-hash xs) >> ; '#hash((width . 10) (foo . bar) (zam . 42)) >> ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; >> >> >> >> >> >> >> >> On Sat, Jan 24, 2015 at 9:27 AM, Sam Tobin-Hochstadt >> <sa...@cs.indiana.edu> wrote: >>> >>> On Sat, Jan 24, 2015 at 12:06 PM, Matthew Butterick <m...@mbtype.com> >>> wrote: >>> > Of course, developer time is limited, so I'm always reluctant to post >>> > comments amounting to "it would be nice if someone else did >>> > such-and-such >>> > for me ..." In this case I simply don't have the experience with TR to >>> > know >>> > where the major breaks with idiomatic Racket occur. >>> > >>> > But user time is limited too. In my case, I'm trying to decide whether >>> > TR is >>> > a cost-effective upgrade for my Racket program. What I can't figure out >>> > is >>> > whether `hash` is an outlier, or the tip of the iceberg, because today, >>> > I'm >>> > a complete idiot about TR. >>> >>> For this issue, Alex just submitted a patch, so it will be fixed soon. >>> >>> In general, TR doesn't work well with functions like `hash` that take >>> their arguments in pairs or triples, and thus they end up having >>> simpler types than the full Racket behavior. >>> >>> Sam >>> >>> > >>> > >>> > >>> > >>> > On Sat, Jan 24, 2015 at 9:01 AM, Matthew Butterick <m...@mbtype.com> >>> > wrote: >>> >> >>> >> Of course, developer time is limited, so I'm always reluctant to post >>> >> comments amounting to "it would be nice if someone else did >>> >> such-and-such >>> >> for me ..." In this case I simply don't have the experience with TR to >>> >> know >>> >> where the major breaks with idiomatic Racket occur. >>> >> >>> >> But user time is limited too. In my case, I'm trying to decide whether >>> >> TR >>> >> is a cost-effective upgrade for my Racket program. What I can't figure >>> >> out >>> >> is whether `hash >>> >> >>> >> >>> >> On Sat, Jan 24, 2015 at 7:13 AM, Robby Findler >>> >> <ro...@eecs.northwestern.edu> wrote: >>> >>> >>> >>> It seems like a small step to start by documenting the ones that >>> >>> people trip up against multiple times in our mailing lists. >>> >>> >>> >>> Robby >>> >>> >>> >>> On Sat, Jan 24, 2015 at 9:07 AM, Matthias Felleisen >>> >>> <matth...@ccs.neu.edu> wrote: >>> >>> > >>> >>> > On Jan 24, 2015, at 1:43 AM, Matthew Butterick wrote: >>> >>> > >>> >>> > FWIW, Sam's point that one can't expect every untyped program to >>> >>> > work >>> >>> > without modification is entirely fair. >>> >>> > >>> >>> > >>> >>> > Correct. >>> >>> > >>> >>> > But Konrad's point is also fair: if a function like `append` or >>> >>> > `hash` >>> >>> > works >>> >>> > differently in TR, then it is, for practical purposes, not the same >>> >>> > function, even if it relies on the same code. >>> >>> > >>> >>> > >>> >>> > This statement is too coarse. There are at least two senses in >>> >>> > which a >>> >>> > TR >>> >>> > function f is distinct from an R function: >>> >>> > >>> >>> > 1. f's type restricts the usability of f to a strict "subset" [in >>> >>> > the >>> >>> > naive >>> >>> > set-theoretic sense]. This is most likely due to a weakness of the >>> >>> > type >>> >>> > system; the language of "theorems" isn't strong enough to express >>> >>> > R's >>> >>> > intention w/o making the inference rules unsound. [Unlike in the >>> >>> > legal >>> >>> > world, In PL arguments of 'typedness' must be about truly-guilty or >>> >>> > not-guilty. The rulings are completely impartial and uniform, i.e., >>> >>> > totally >>> >>> > fair.] >>> >>> > >>> >>> > 2. f's type ___changes___ the meaning of the code. (That's also >>> >>> > possible but >>> >>> > I don't want to fan the argument that Sam and I have about this.) >>> >>> > >>> >>> > >>> >>> > If it would be superfluous to repeat every TR function in the >>> >>> > documentation, >>> >>> > it still could be valuable to document some of the major departures >>> >>> > from >>> >>> > Racket. I mean, I would read that, for sure ;) >>> >>> > >>> >>> > >>> >>> > >>> >>> > Actually it would not be superfluous. We just don't have the >>> >>> > manpower >>> >>> > but >>> >>> > perhaps it's time to tackle this problem (perhaps in a >>> >>> > semi-automated >>> >>> > manner). >>> >>> > >>> >>> > -- Matthias >>> >>> > >>> >>> > >>> >>> > ____________________ >>> >>> > Racket Users list: >>> >>> > http://lists.racket-lang.org/users >>> >>> > >>> >> >>> >> >>> > >>> > >>> > ____________________ >>> > Racket Users list: >>> > http://lists.racket-lang.org/users >>> > >> >> >> ____________________ >> Racket Users list: >> http://lists.racket-lang.org/users >> >> > > > ____________________ > Racket Users list: > http://lists.racket-lang.org/users > ____________________ Racket Users list: http://lists.racket-lang.org/users
