<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div>If you wanted a loose enough type to do that, this would probably still be useful:</div><div><br></div><div><div dir="ltr"><div>#lang typed/racket</div><div>(: mb-hash : (All (a) [(Listof a) . -> . (HashTable a a)]))</div><div>(define (mb-hash xs)</div><div> (let loop ([hsh : (HashTable a a) (hash)] [xs : (Listof a) 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></div><br><div><div>On Jan 24, 2015, at 8:31 PM, Matthew Butterick <<a href="mailto:mb@mbtype.com">mb@mbtype.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div dir="ltr">OIC — at compile time, all that's known about `make-list` is that it will produce some kind of list, so that's the strictest type that will check. Therefore the (only?) way to make this work is to loosen the types accordingly:<div><br></div><div><div>#lang typed/racket</div><div>(: mb-hash : ((Listof Any) . -> . (HashTable Any Any)))</div><div>(define (mb-hash xs)</div><div> (let loop ([hsh : (HashTable Any Any) (hash)] [xs : (Listof Any) 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 succeeds</div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Jan 24, 2015 at 5:21 PM, 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:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">This happens because xs and ys don't actually have the same type. The<br>
REPL in TR provides the information:<br>
<br>
> xs<br>
- : (Listof 'a) [more precisely: (List 'a 'a)]<br>
'(a a)<br>
> ys<br>
- : (Listof 'a)<br>
'(a a)<br>
<br>
It's that "more precisely" bit that's crucial. TR knowns that xs has<br>
exactly two elements, but it doesn't know that about `ys` (because it<br>
doesn't have fancy types for `make-list`, and in fact can't expresses<br>
them even if we wanted to).<br>
<span class="HOEnZb"><font color="#888888"><br>
Sam<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
On Sat, Jan 24, 2015 at 8:15 PM, Matthew Butterick <<a href="mailto:mb@mbtype.com">mb@mbtype.com</a>> wrote:<br>
> Thank you for the tip. I'm afraid I'm still unclear why this happens,<br>
> however:<br>
><br>
> #lang typed/racket<br>
> (: mb-hash : (All (A B) (Rec lst (U Null (List* A B lst))) -> (HashTable A<br>
> B)))<br>
> (define (mb-hash xs)<br>
> (let loop ([hsh : (HashTable A B) (hash)] [xs : (Rec lst (U Null (List* A<br>
> B lst))) xs])<br>
> (match xs<br>
> [(list) hsh]<br>
> [(list-rest a b rst) (loop (hash-set hsh a b) rst)])))<br>
><br>
> (define xs '(a a))<br>
> (define ys (make-list 2 'a))<br>
><br>
> xs ; (Listof 'a)<br>
> ys ; (Listof 'a)<br>
><br>
> (mb-hash xs) ; typecheck succeeds<br>
> (mb-hash ys) ; typecheck fails<br>
><br>
><br>
><br>
><br>
><br>
> On Sat, Jan 24, 2015 at 1:10 PM, Alexander D. Knauth <<a href="mailto:alexander@knauth.org">alexander@knauth.org</a>><br>
> wrote:<br>
>><br>
>> For something like that, this works, and supports polymorphism, checks an<br>
>> even number of elements, and separates the key types from the value types:<br>
>> #lang typed/racket<br>
>> (: mb-hash : (All (A B) (Rec lst (U Null (List* A B lst))) -> (HashTable A<br>
>> B)))<br>
>> (define (mb-hash xs)<br>
>> (let loop ([hsh : (HashTable A B) (hash)] [xs : (Rec lst (U Null (List*<br>
>> A B lst))) xs])<br>
>> (match xs<br>
>> [(list) hsh]<br>
>> [(list-rest a b rst) (loop (hash-set hsh a b) rst)])))<br>
>> (define xs '(width 10 foo bar zam 42))<br>
>> (mb-hash xs)<br>
>> ;'#hash((width . 10) (foo . bar) (zam . 42))<br>
>><br>
>> Before the repo was split, there was a pull request by Asumu Takikawa<br>
>> here:<br>
>> <a href="https://github.com/plt/racket/pull/564" target="_blank">https://github.com/plt/racket/pull/564</a><br>
>> which would allow something like this to be used for a type for hash,<br>
>> where the arguments wouldn’t have to be in a list like this.<br>
>><br>
>> On Jan 24, 2015, at 2:50 PM, Matthew Butterick <<a href="mailto:mb@mbtype.com">mb@mbtype.com</a>> wrote:<br>
>><br>
>>> 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>
>><br>
>><br>
>><br>
>> In my case, I've already committed to indefinite-arity `hash` as part of<br>
>> the program interface (a decision I could reconsider, though it would<br>
>> require a new quantum of benefit to be worthwhile)<br>
>><br>
>> Am I wrong that this TR function approximates the standard `hash` (by<br>
>> unpacking the arguments manually)?<br>
>><br>
>> If not, is this approach disfavored for some other reason?<br>
>><br>
>> ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;<br>
>> #lang typed/racket/base<br>
>><br>
>> (: mb-hash ((Listof Any) . -> . HashTableTop))<br>
>> (define (mb-hash xs)<br>
>> (let-values ([(ks vs even?) (for/fold<br>
>> ([ks : (Listof Any) null][vs : (Listof Any)<br>
>> null][even? : Boolean #t])<br>
>> ([x (in-list xs)])<br>
>> (if even?<br>
>> (values (cons x ks) vs #f)<br>
>> (values ks (cons x vs) #t)))])<br>
>> (when (not even?) (error 'bad-input))<br>
>> (for/hash ([k (in-list ks)][v (in-list vs)])<br>
>> (values k v))))<br>
>><br>
>> (define xs '(width 10 foo bar zam 42))<br>
>> (mb-hash xs)<br>
>> ; '#hash((width . 10) (foo . bar) (zam . 42))<br>
>> ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;<br>
>><br>
>><br>
>><br>
>><br>
>><br>
>><br>
>><br>
>> On Sat, Jan 24, 2015 at 9:27 AM, Sam Tobin-Hochstadt<br>
>> <<a href="mailto:samth@cs.indiana.edu">samth@cs.indiana.edu</a>> wrote:<br>
>>><br>
>>> On Sat, Jan 24, 2015 at 12:06 PM, Matthew Butterick <<a href="mailto:mb@mbtype.com">mb@mbtype.com</a>><br>
>>> 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<br>
>>> > such-and-such<br>
>>> > for me ..." In this case I simply don't have the experience with TR to<br>
>>> > 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<br>
>>> > TR is<br>
>>> > a cost-effective upgrade for my Racket program. What I can't figure out<br>
>>> > is<br>
>>> > whether `hash` is an outlier, or the tip of the iceberg, because today,<br>
>>> > I'm<br>
>>> > a complete idiot about TR.<br>
>>><br>
>>> 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>
>>><br>
>>> Sam<br>
>>><br>
>>> ><br>
>>> ><br>
>>> ><br>
>>> ><br>
>>> > On Sat, Jan 24, 2015 at 9:01 AM, Matthew Butterick <<a href="mailto:mb@mbtype.com">mb@mbtype.com</a>><br>
>>> > 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<br>
>>> >> such-and-such<br>
>>> >> for me ..." In this case I simply don't have the experience with TR to<br>
>>> >> 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<br>
>>> >> TR<br>
>>> >> is a cost-effective upgrade for my Racket program. What I can't figure<br>
>>> >> 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">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">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<br>
>>> >>> > 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<br>
>>> >>> > `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<br>
>>> >>> > 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<br>
>>> >>> > the<br>
>>> >>> > naive<br>
>>> >>> > set-theoretic sense]. This is most likely due to a weakness of the<br>
>>> >>> > type<br>
>>> >>> > system; the language of "theorems" isn't strong enough to express<br>
>>> >>> > R's<br>
>>> >>> > intention w/o making the inference rules unsound. [Unlike in the<br>
>>> >>> > 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<br>
>>> >>> > manpower<br>
>>> >>> > but<br>
>>> >>> > perhaps it's time to tackle this problem (perhaps in a<br>
>>> >>> > 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>
>><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>
> 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>
____________________<br> Racket Users list:<br> <a href="http://lists.racket-lang.org/users">http://lists.racket-lang.org/users</a><br></blockquote></div><br></body></html>