Re: [racket-users] (curry map string->number) in Typed Racket
On Wed, Aug 28, 2019 at 9:58 AM Štěpán Němec 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.
Re: [racket-users] (curry map string->number) in Typed Racket
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 -- 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/87blw9gzo0.fsf%40gmail.com.
Re: [racket-users] (curry map string->number) in Typed Racket
On Wed, Aug 28, 2019 at 5:59 AM Štěpán Němec 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 ), 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.
Re: [racket-users] (curry map string->number) in Typed Racket
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 -- 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/87ftllhaq5.fsf%40gmail.com.
Re: [racket-users] (curry map string->number) in Typed Racket
(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 On Thu, Aug 22, 2019 at 4:15 PM Štěpán Němec wrote: > > > 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 > > -- > 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/8736hths88.fsf%40gmail.com. -- 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/CAKfDxxwOSK%3DAg0tw%3DtQgvZ9sRrnXt_J7YSz12V1wvLYRusfOzQ%40mail.gmail.com.
[racket-users] (curry map string->number) in Typed Racket
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 -- 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/8736hths88.fsf%40gmail.com.
