(curry map string->number) in Typed Racket

[Štěpán Němec]

I have a hard time persuading Typed Racket to accept the expression
"(curry map string->number)". No amount of type annotations or added
`inst`s (as recommended by the guide[1]) I could come up with seem to
help.

Is there a way to make it work?

[1] https://docs.racket-lang.org/ts-guide/caveats.html#%28part._.Type_inference_for_polymorphic_functions%29

Here's an example with a bit more context (solely for illustration
purposes; I couldn't make the simple expression above work even
isolated):

(match-let ([(pregexp "#\\d+ +@ +(\\d+),(\\d+): +(\\d+)x(\\d+)"
(list-rest _ (app (curry map string->number)
(list x y dx dy))))
"#1299 @ 414,871: 29x11"])
x)

Thank you,

Štěpán

[Jon Zeppieri]

(curry (inst map (U Complex False) String)
string->number)

... typechecks, but in your expression, you're going to need to handle
the possibility that the pattern variables in `list-rest` pattern are
#f.

- Jon

> --
> 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/8736hths88.fsf%40gmail.com.

[Štěpán Němec]

On Thu, 22 Aug 2019 16:40:03 -0400
Jon Zeppieri wrote:

> (curry (inst map (U Complex False) String)
> string->number)
>
> ... typechecks, but in your expression, you're going to need to handle
> the possibility that the pattern variables in `list-rest` pattern are
> #f.

Many thanks for the help. I find it quite confusing, though: I'd expect
something like "(inst map (-> String (U Complex False)) (Listof String))",
which apparently means something else...

Does that mean that for higher-order function parameters, inst expects
only the return type signature, not that of the function itself? But
what about the String instead of (Listof String)? Or is this some kind
of special case for functions like map? Is it documented somewhere?

And more generally, could you recommend any good learning resources (or
good non-trivial code examples) of Typed Racket usage? I have read the
guide and consulted the reference, but keep hitting the wall...

Thanks,

Štěpán

[Jon Zeppieri]

On Wed, Aug 28, 2019 at 5:59 AM Štěpán Němec <ste...@gmail.com> wrote:
>
> On Thu, 22 Aug 2019 16:40:03 -0400
> Jon Zeppieri wrote:
>
> > (curry (inst map (U Complex False) String)
> > string->number)
> >
> > ... typechecks, but in your expression, you're going to need to handle
> > the possibility that the pattern variables in `list-rest` pattern are
> > #f.
>
> Many thanks for the help. I find it quite confusing, though: I'd expect
> something like "(inst map (-> String (U Complex False)) (Listof String))",
> which apparently means something else...

Let's look at the type of `map`:

> map
- : (All (c a b ...)
(case->
(-> (-> a c) (Pairof a (Listof a)) (Pairof c (Listof c)))
(-> (-> a b ... b c) (Listof a) (Listof b) ... b (Listof c))))

We're only interested in the two-argument case (though we do want to
admit empty lists) so we can treat that as if it were:

(All (c a) (-> (-> a c) (Listof a) (Listof c))) [*]

There are two type variables to instantiate: c and a, and they need to
be instantiated in that order -- in the order they are bound by the
universal quantifier (`All`). The first argument to `map` is a
function of type (-> a c). In our case, that function will be
`string->number`, so now we need to know the type of `string->number`:

> string->number
- : (->* (String) (Number) (U Complex False))

It has an optional argument of type Number, but we don't need that, so
we're going to ignore it and treat this as if it were simply:

(-> String (U Complex False))

Remember, we were looking for a function of type:
(-> a c)
and we found one of type:

(-> String (U Complex False))

That means that `a` will be instantiated by `String` and `c` will be
instantiated by `(U Complex False)`. But recall the order that the
variables are bound by the universal quantifier: (All (c a) ...). So
we need to do:
(inst map <instantiation of c> <instantiation of a>), which is:

(inst map (U Complex False) String)

>

> Does that mean that for higher-order function parameters, inst expects
> only the return type signature, not that of the function itself?

The main point here is that `inst` needs substitutions for the type
_variables_, not for the types of the function arguments.

> But what about the String instead of (Listof String)? Or is this some kind
> of special case for functions like map? Is it documented somewhere?

This is a good illustration of what I just wrote: the type for `map`
that we wrote above requires a `(Listof a)`. Our job is to instantiate
the variable `a`. The `Listof` part is already there.

>
> And more generally, could you recommend any good learning resources (or
> good non-trivial code examples) of Typed Racket usage? I have read the
> guide and consulted the reference, but keep hitting the wall...

I'm afraid I can't help you with examples, but I bet some other people
on this list can.

- Jon

[*] The cases in the type of `map` are a bit confusing because, at
first glance, it looks like the first case is for the two-argument
version of `map`, whereas the second is for the vararg version. But
really the first version is for the two-argument version that is given
a non-empty list as the second argument (and therefore also returns a
non-empty list).

[Štěpán Němec]

On Wed, 28 Aug 2019 09:23:03 -0400
Jon Zeppieri wrote:

[...]

>> Does that mean that for higher-order function parameters, inst expects
>> only the return type signature, not that of the function itself?
>
> The main point here is that `inst` needs substitutions for the type
> _variables_, not for the types of the function arguments.

Oh, _now_ it makes sense! I see now that I really misunderstood even the
example in the reference entry for `inst`: I took "(inst cons Integer
Integer)" to mean "two Integer args" (which of course would only account
for the (Pairof a b) case and doesn't make sense in the context) instead
of "two Integer type variables".

Thank you for the detailed explanation!

--
Štěpán

[Jon Zeppieri]

Glad to help. I don't know if you're familiar with System F, but if
you are, then you can think of `inst` as function application for
capital lambda (Λ) functions (functions that map types to terms). So,
a simplified version of map would look something like this (if Typed
Racket had explicit Λ functions):

(define map
(Λ (c a)
(λ ([fn : (-> a c)]
[lst: (Listof a)])
...)))

So, when you do `(inst map (U Complex False) String)`, you're applying
the outer Λ function, so that `c` and `a` get replaced in the body of
the function by `(U Complex False)` and `String`, respectively, and
you end up with:

(λ ([fn : (-> String (U Complex False))]
[lst: (Listof String)])
...)

- Jon