Re: [racket-users] (curry map string->number) in Typed Racket

2019-08-28 Thread Jon Zeppieri
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

2019-08-28 Thread Š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

-- 
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

2019-08-28 Thread Jon Zeppieri
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

2019-08-28 Thread Š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

-- 
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

2019-08-22 Thread 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

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.