Re: [racket-users] hash-ref in typed Racket

[Sam Tobin-Hochstadt]

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  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: # key: string value: String value
> key: missing value: Missed!
>
> Thunk on error:
> key: function value: # 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  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  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  wrote:
>
>
> For the type of the third argument, rather than "any non-function", could 
> Typed Racket use the type of the 

Re: [racket-users] hash-ref in typed Racket

[Tim Jervis]

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: #
 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  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 > > 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 > > 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 >>> > 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?)
>