[racket] Type of curry

The type of curry is correct, but imprecise.  It does not express all
possible uses of curry.  The curry function can be used to split any
function application into an arbitrary number of stages, each with an
arbitrary number of arguments.  There is no way to write down that type.
Typed Racket needs to know how many stages there are to the function
application -- that's the nesting level of "->" -- and how many arguments
all but the last step take -- because there can be only one "..." in the
initial function type, and it must be at the end of the arguments.

Right now the type is specialized to two stages, each with one argument.
It could be generalized a bit further -- perhaps to allow arbitrary
arguments at the second stage, or to allow two arguments at the first
stage, or to allow a three-stage case as well, or some combination
thereof.  However, this specialization can only go to some arbitrary,
finite degree without changing the type system, and each addition will
complicate the type of curry used in error messages.

For now, that means you will have to define f1a explicitly, or write a more
specific instantiation of curry for your uses.  In the future, perhaps the
TR implementers can broaden the type of curry a bit.  Types for this kind
of higher-order function are an area of open research for TR, so perhaps
things will get better in the future.

Carl Eastlund


On Sun, Feb 24, 2013 at 5:59 PM, Norman Gray <norman at astro.gla.ac.uk> wrote:

>
> Greetings,
>
> Is the type of 'curry' correct?
>
> #lang typed/racket
>
> (: f2 (Boolean Integer Integer -> Integer))
> (define (f2 add? i1 i2)
>   (if add?
>       (+ i1 i2)
>       (- i1 i2)))
>
> (define f1a (curry f2 #t)) ; fails to typecheck
>
> (f2 #t 2 3)
> (f2 #f 2 1)
> ;(f1a 10 20)
>
> ===>
>
> Welcome to DrRacket, version 5.3.3 [3m].
> Language: typed/racket; memory limit: 128 MB.
> . Type Checker: Polymorphic function curry could not be applied to
> arguments:
> Domains: (a b -> c)
>          (a b -> c) a
> Arguments: (Boolean Integer Integer -> Integer) True
>  in: (curry f2 #t)
> >
>
> It works fine when currying a two-argument function.
>
> All the best,
>
> Norman
> (I'll resist any vindaloo jokes)
>
>
> --
> Norman Gray  :  http://nxg.me.uk
> SUPA School of Physics and Astronomy, University of Glasgow, UK
>
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20130225/d44d4441/attachment.html>