[racket] Typed Racket frustration

Polymorphic types generate impersonator contracts for the type
variables (a and b, here). Contracts for hashes (such as `hash/c`)
don't accept impersonator contracts on keys.

Sam

On Thu, Oct 30, 2014 at 3:22 PM, Alexander D. Knauth
<alexander at knauth.org> wrote:
> What I did to get around this was use require/typed with a more useful type,
> but when I tried it again just now it didn’t work any more.  This used to
> work, what changed?   And why would it expect a flat contract anywhere?
>
> #lang typed/racket
>
> (require/typed racket/base
>                [hash (All (a b)
>                           (case-> [-> (HashTable a b)]
>                                   [a b -> (HashTable a b)]
>                                   [a b a b -> (HashTable a b)]
>                                   [a b a b a b -> (HashTable a b)]
>                                   [a b a b a b a b -> (HashTable a b)]
>                                   [a b a b a b a b a b -> (HashTable a b)]
>                                   [a b a b a b a b a b a b -> (HashTable a
> b)]
>                                   [a b a b a b a b a b a b a b -> (HashTable
> a b)]
>                                   [a b a b a b a b a b a b a b a b ->
> (HashTable a b)]
>                                   ))])
>
> (hash 1 2)
>
> . Type Checker: Type (All (a b) (case-> (-> (HashTable a b)) (-> a b
> (HashTable a b)) ....)) could not be converted to a contract: required a
> flat contract but generated an impersonator contract in: (All (a b) (case->
> (-> (HashTable a b)) (-> a b (HashTable a b)) ....))
>
> On Oct 30, 2014, at 7:53 AM, Konrad Hinsen <konrad.hinsen at fastmail.net>
> wrote:
>
> Sam Tobin-Hochstadt writes:
>
> This isn't a different version of `hash` -- instead, it's the same
> version, with a type that doesn't accept every working untyped Racket
> program.
>
>
> This make sense from the point of view of the language implementation,
> but not from the point of view of the language user.
>
> For me as a programmer, Typed Racket is a different language from
> Racket, because a valid program in one language is not a valid program
> in the other. Whether or not Typed Racket's hash ends up calling
> plain Racket's hash is an implementation detail I don't care about,
> except perhaps when dealing with interfacing modules in the two
> languages.
>
> From this point of view, Typed Racket is to a large degree an
> undocumented language. Much of the documentation simply points to the
> one of plain Racket, which doesn't fully apply. Moreover, there is no
> simple set of rules that would let me deduce Typed Racket's API (which
> includes types) from plain Racket's API.
>
> The type of `hash` is one that comes up a bunch, and we should
> probably just add a few special cases that handle 2/4/6 arguments.
> Unfortunately, we don't yet have a mechanism for fully supporting the
> behavior of `hash`, and so there will be cases that work in untyped
> Racket but not in Typed Racket.
>
>
> I wouldn't expect the type checker to support all working plain Racket
> code. But I do expect Typed Racket to provide equivalent (though
> possibly syntactically different) APIs for common tasks such as
> creating an immutable hash table from key-value pairs.
>
> I suppose the problem with hash is the indefinite number of arguments.
> One way out is a list of key-value pairs, with hash becoming the inverse
> of hash->list. It's certainly much easier to port untyped code to such a
> somewhat different syntax than to have no straightforward option at all.
>
> This is BTW what I used as a workaround:
>
>   (: list->hash (All (a b) (-> (Listof (Pairof a b)) (HashTable a b))))
>   (define (list->hash lst)
>     (for/fold ([hsh : (HashTable a b) (hash)])
>               ([kv : (Pairof a b) lst])
>       (hash-set hsh (car kv) (cdr kv))))
>
> Konrad.
> ____________________
>  Racket Users list:
>  http://lists.racket-lang.org/users
>
>