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