index-of + TR ... parametricity problem?

[John Clements]

It looks like my quick attempt at importing index-of into TR is running into a problem. Here’s the program I ran:

#lang typed/racket

(require/typed racket/list
[index-of (All (T) ((Listof T) T -> (U False Natural)))])

(index-of '(n s e w) 'n) ;; returns... #f?

In typed/racket/no-check this returns 0, and also in racket (mutatis mutandis).

I thought this might be some kind of parametricity issue, but even when I instantiate index-of at Symbol which should pretty much clear the way for arbitrary equality checking, I still get False.

Am I missing something obvious? Maybe I shouldn’t be running from the November 14 git head any more?

Welcome to DrRacket, version 7.5.0.7--2019-11-14(-/f) [3m].

John

[Sam Tobin-Hochstadt]

Yes, this is because the contract enforces parametericity, which
doesn't allow `index-of` to work the way you'd want.

Instantiating things doesn't help because the contract is based on the
`require/typed`, not on the use site.

Here's a few suggestions:

1. Submit a pull-request to TR to add `index-of`
2. Import `index-of` at a concrete type
3. Use `unsafe-require/typed`
4. Use the third argument to `index-of?`

Sam

> --
> 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/ef401a3d-9c41-44f9-ba61-93c09065755e%40mtasv.net.

[John Clements]

Oh! of course. Makes sense.

If I make a pull request, does that mean I get a pass for wasting my time doing advent of code?

John