That particular pattern, with `(U String (-> String))`, will work, but your generalized version would be wrong if it worked. Consider:
``` (: unsound : (Immutable-HashTable Symbol (-> String)) -> String) (define (unsound h) ((hash-ref h (gensym) (lambda () "x")))) (unsound (hash)) ``` This program type checks with your second `require/typed` of `hash-ref`, but it's wrong. We can see that by using `unsafe-require/typed`, and we get an error because we can't apply "x". Furthermore, you can't generalize to (U T (-> T) either, because if T is (-> String) then you get the same problem. Sam On Wed, Nov 25, 2020 at 7:28 AM Tim Jervis <tim.jer...@gmail.com> wrote: > > For the record, this seems to work fine: > > #lang typed/racket > > (require/typed racket > [hash-ref ((Immutable-HashTable Symbol > (U (-> String) > String)) > Symbol > (U String > (-> String)) > -> > (U String > (-> String)))]) > > (let* ([h : (Immutable-HashTable Symbol > (U (-> String) > String)) > (make-immutable-hash)] > [h (hash-set h > 'function > (thunk "Function value"))] > [h (hash-set h > 'string > "String value")]) > > (printf "Fixed string on error:\n") > (for ([key (in-list '(function string missing))]) > (printf "key: ~a\tvalue: ~a\n" > key > (hash-ref h > key > "Missed!"))) > (printf "\n") > > (printf "Thunk on error:\n") > (for ([key (in-list '(function string missing))]) > (printf "key: ~a\tvalue: ~a\n" > key > (hash-ref h > key > (thunk "Missed!"))))) > > > > > > > Fixed string on error: > key: function value: #<procedure:... > key: string value: String value > key: missing value: Missed! > > Thunk on error: > key: function value: #<procedure:... > key: string value: String value > key: missing value: Missed! > > > > > > > but this attempt to generalise fails: > > #lang typed/racket > > (require/typed racket > [hash-ref (All (K V) > (Immutable-HashTable K V) > K > V > -> > V)]) > > (let* ([h : (Immutable-HashTable Symbol > (U (-> String) > String)) > (make-immutable-hash)] > [h (hash-set h > 'function > (thunk "Function value"))] > [h (hash-set h > 'string > "String value")]) > > (printf "Fixed string on error:\n") > (for ([key (in-list '(function string missing))]) > (printf "key: ~a\tvalue: ~a\n" > key > (hash-ref h > key > "Missed!"))) > (printf "\n") > > (printf "Thunk on error:\n") > (for ([key (in-list '(function string missing))]) > (printf "key: ~a\tvalue: ~a\n" > key > (hash-ref h > key > (thunk "Missed!"))))) > > > > > > ; hash/c: contract violation > ; expected: chaperone-contract? > ; given: K4 > > > On 24 Nov 2020, at 15:20, Tim Jervis <tim.jer...@gmail.com> wrote: > > Wouldn’t that possibility then have to be part of the type for the values in > the hash? Maybe I don’t understand how types work for hashes. > > In this code: > > #lang typed/racket > > (define h : (Immutable-HashTable Integer (-> String)) > (make-immutable-hash)) > > (hash-ref h > 2 > (thunk "Hit and miss")) > > > I think I’ve set the type of the values of the hash h to be a thunk that > returns a string. I’m then trying to access a key in that hash, which misses > because the hash has no keys. The third argument works because it’s a > function that happens to return a string. It’s funny because it looks like it > type-checks, but it doesn’t really. > > This code: > > #lang typed/racket > > (define h : (Immutable-HashTable Integer String) > (make-immutable-hash)) > > (hash-ref h > 2 > (thunk "Hit and miss")) > > > also type-checks because even though the third argument to hash-ref is not a > String, it is a function. > > Oddly, to me at least, > > #lang typed/racket > > (define h : (Immutable-HashTable Integer String) > (make-immutable-hash)) > > (hash-ref h > 2 > "Hit and miss") > > > Does not type check even though the type of the hash’s values is String, the > same as the third argument of hash-ref. > > On 24 Nov 2020, at 14:44, Sam Tobin-Hochstadt <sa...@cs.indiana.edu> wrote: > > Unfortunately, that doesn't work -- the values in the hash could > include functions. > > Sam > > On Tue, Nov 24, 2020 at 7:25 AM Tim Jervis <tim.jer...@gmail.com> wrote: > > > For the type of the third argument, rather than "any non-function", could > Typed Racket use the type of the values in the hash? > > On Tuesday, 21 April 2020 at 15:51:00 UTC+1 Sam Tobin-Hochstadt wrote: > > > The problem here is with the optional third argument to `hash-ref`. > Typed Racket only allows `#f` or functions as the third argument. > Plain Racket allows any non-function value as a default, or a function > which is called to produce the default. Since "any non-function" is > not expressible in Typed Racket, it's more restricted here. > > The best option is to wrap the third argument in a thunk: `(lambda () > 'other)`. > > As an aside, you probably don't want to use `cast` this extensively in > your program. > > Sam > > On Tue, Apr 21, 2020 at 10:35 AM Hendrik Boom <hen...@topoi.pooq.com> wrote: > > > In typed Racket I define a hashtable: > > (: vector-to-contract (HashTable TType CContract)) > > (define vector-to-contract > (make-hash > (cast '( > (_bytes . bytes?) > (_s8vector . s8vector?) > (_u16vector . u16vector?) > (_s16vector . s16vector?) > (_u32vector . u32vector?) > (_s32vector . s32vector?) > (_u64vector . u64vector?) > (_s64vector . s64vector?) > (_f32vector . f32vector?) > (_f64vector . f64vector?)) > (Listof (Pair TType CContract)) > ) > )) > > And then I try to look something up in it: > > ( hash-ref vector-to-contract (cast '_bytes TType) (cast 'other CContract)) > > and I am informed that I cannot, it seems, look up a value of type > TType in a hastable whose type indicates it looks up things of type > TType: > > Type Checker: Polymorphic function `hash-ref' could not be applied to > arguments: > Types: HashTableTop a (-> c) -> Any > HashTableTop a False -> Any > HashTableTop a -> Any > Arguments: (HashTable TType CContract) TType CContract > Expected result: AnyValues > in: (hash-ref vector-to-contract (cast (quote _bytes) TType) (cast > (quote other) CContract)) > > > How *does* one use hashtables in typed Racket? > > -- hendrik > > -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to racket-users...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/racket-users/20200421143453.lauuqi3pb4fdgyhh%40topoi.pooq.com. > > > -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to racket-users+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/racket-users/aacb7226-8a0e-4fe0-9481-c1f72143eec2n%40googlegroups.com. > > > > -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to racket-users+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/racket-users/2F152CB5-E6E3-4C8F-B11F-0477DF2DD965%40gmail.com. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAK%3DHD%2BbYTqAo-HubpgnknefyhsMAXnKVYBAUfXKgN6ApMN55kg%40mail.gmail.com.
