On Wed, Aug 28, 2019 at 9:58 AM Štěpán Němec <step...@gmail.com> wrote:
>
> 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!
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
--
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/CAKfDxxzCYi58qMh1%3DZDhk6_marB_5JD_10do9FHOnGcA5RerjQ%40mail.gmail.com.
