[racket] Typed Racket frustration

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 <alexander at 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 <mb at 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 <samth at cs.indiana.edu
> > wrote:
>
>> On Sat, Jan 24, 2015 at 12:06 PM, Matthew Butterick <mb at 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 <mb at 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
>> >> <robby at 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
>> >>> <matthias at 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
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20150124/5303220a/attachment-0001.html>