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

2020-11-25 Thread 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 va

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

2020-11-25 Thread 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?)
> (_s16vecto

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

2020-11-24 Thread Tim Jervis
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?)
 (_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/2B6A277A-5538-4FFB-86E7-48F3D663C90D%40gmail.com.


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

2020-11-24 Thread Sam Tobin-Hochstadt
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?)
>> > (_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/CAK%3DHD%2BZZU4mNFX1XnfFXYxHjv8baaPw%3DZ%3D-ArO4tNhE%3D7VKqzQ%40mail.gmail.com.


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

2020-11-24 Thread Tim Jervis
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?)
> > (_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.


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

2020-04-21 Thread Hendrik Boom
On Tue, Apr 21, 2020 at 10:50:44AM -0400, 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.

I missed that.  Thanks.

> 
> 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.

No, I don't.  I hoped it would help, but I was fixing the wrong problem, 
so it didn't .

-- hendrik

> 
> 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?)
> >(_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+unsubscr...@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/CAK%3DHD%2BY-pc3Jfg4RgRmAPMqSUxUj8rJsm3np2eq2%2B-J5PWTO4Q%40mail.gmail.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/20200421163253.ui4xuokcgsprhyna%40topoi.pooq.com.


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

2020-04-21 Thread Sam Tobin-Hochstadt
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?)
>(_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+unsubscr...@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/CAK%3DHD%2BY-pc3Jfg4RgRmAPMqSUxUj8rJsm3np2eq2%2B-J5PWTO4Q%40mail.gmail.com.


[racket-users] hash-ref in typed Racket

2020-04-21 Thread Hendrik Boom
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/20200421143453.lauuqi3pb4fdgyhh%40topoi.pooq.com.