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]
>> <mailto:[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]
>> <mailto:[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]
>>>> <http://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 [email protected] <http://googlegroups.com/>.
>>>>> To view this discussion on the web visit
>>>>> https://groups.google.com/d/msgid/racket-users/20200421143453.lauuqi3pb4fdgyhh%40topoi.pooq.com
>>>>>
>>>>> <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]
>>> <mailto:[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
>>>
>>> <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.
