[racket] Typed Racket frustration

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:

#lang typed/racket
(: mb-hash : ((Listof Any) . -> . (HashTable Any Any)))
(define (mb-hash xs)
  (let loop ([hsh : (HashTable Any Any) (hash)] [xs : (Listof Any) 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 succeeds

On Sat, Jan 24, 2015 at 5:21 PM, 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
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20150124/4eb1c0f3/attachment-0001.html>