[racket] Typed Racket frustration

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 <mb at 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 <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
>>
>>
>
>
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users
>