On Wed, Aug 28, 2019 at 5:59 AM Štěpán Němec <step...@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).
--
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/CAKfDxxwFSZSXHrhSWjhyaRZa6c%2BtsQK8E%3D1tH56C4K%3D8H71nPA%40mail.gmail.com.
