[racket] Typed Racket frustration

For additional clarification, the point is that the size of the list in `make-list` can be dynamically-determined at runtime, so the type system has no way of getting that information except in the simplest of cases (which it isn’t worth special-casing for, and the type system as-is has no way of adding such special cases even if it were desired).

> On Jan 24, 2015, at 17:21, Sam Tobin-Hochstadt <samth at cs.indiana.edu> wrote:
> 
> 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
>> 
> 
> ____________________
>  Racket Users list:
>  http://lists.racket-lang.org/users