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.