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 <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 [email protected]. > 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 [email protected]. > 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 [email protected]. > 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAK%3DHD%2BbYTqAo-HubpgnknefyhsMAXnKVYBAUfXKgN6ApMN55kg%40mail.gmail.com.
