[plt-scheme] Re: type signature for a multi-parameter function of a fixed number of arguments in Typed Scheme?

On Thu, 16 Oct 2008 06:31:48 -0400, "Carl Eastlund"
<cce at ccs.neu.edu> wrote:

>You can write both multiple-argument and curried functions in Typed
>Scheme, but you have to remember to distinguish the two in your
>definitions and type specifications.  A multiple argument function is
>applied once to multiple arguments, and uses a type signature like (A
>B -> C).  A curried function is applied multiple times, usually to one
>argument each, and uses a type signature like (A -> (B -> C)).  Here
>is code for both that runs without error in Typed Scheme:
>
>#lang typed-scheme
>
>(: regular-plus (Number Number -> Number))
>(define (regular-plus a b)
>  (+ a b))

This works fine:

> (regular-plus 1 2)
- : Number
3

>
>(: curried-plus (Number -> (Number -> Number)))
>(define ((curried-plus a) b)
>  (+ a b))

This requires some care in use.  If I try using it in the same was as
regular-plus, it causes an error message; viz.:

> (curried-plus 1 2)
. typecheck: Too many arguments to function, expected 1, got 2 in:
(curried-plus 1 2)

However, if I treat (curried-plus 1) as a function to be applied to an
argument, say 2, then it works:

> ((curried-plus 1) 2)
- : Number
3
> 

Thank you!  That is exactly what I was seeking.

Now I can write a Typed Scheme version of Towers of Hanoi:

#lang typed-scheme

(: hanoi-typed (Number -> Void))
(define (hanoi-typed n)
  (hanoi-helper-typed 'A 'B 'C n))

(: hanoi-helper-typed (Symbol Symbol Symbol Number -> Void))
(define (hanoi-helper-typed source using destination n)
  (cond ((= n 1)
         (printf "Moving from disc ~a to ~a.\n" source destination))
        (else
         (hanoi-helper-typed source destination using (- n 1))
         (hanoi-helper-typed source using destination 1)
         (hanoi-helper-typed using source destination (- n 1)))))

> (hanoi-typed 1)
Moving from disc A to C.
> (hanoi-typed 2)
Moving from disc A to B.
Moving from disc A to C.
Moving from disc B to C.
> (hanoi-typed 3)
Moving from disc A to C.
Moving from disc A to B.
Moving from disc C to B.
Moving from disc A to C.
Moving from disc B to A.
Moving from disc B to C.
Moving from disc A to C.
> 

Now, here is a curried Typed Scheme version of Towers of Hanoi:

#lang typed-scheme

(: hanoi-curried (Number -> Void))
(define (hanoi-curried n)
  ((((hanoi-helper-curried 'A) 'B) 'C) n))

(: hanoi-helper-curried (Symbol -> (Symbol -> (Symbol -> (Number ->
Void)))))
(define ((((hanoi-helper-curried source) using) destination) n)
  (cond ((= n 1)
         (printf "Moving from disc ~a to ~a.\n" source destination))
        (else
         ((((hanoi-helper-curried source) destination) using) (- n 1))
         ((((hanoi-helper-curried source) using) destination) 1)
         ((((hanoi-helper-curried using) source) destination) (- n
1)))))

> (hanoi-curried 1)
Moving from disc A to C.
> (hanoi-curried 2)
Moving from disc A to B.
Moving from disc A to C.
Moving from disc B to C.
> (hanoi-curried 3)
Moving from disc A to C.
Moving from disc A to B.
Moving from disc C to B.
Moving from disc A to C.
Moving from disc B to A.
Moving from disc B to C.
Moving from disc A to C.
> 

This is fun!  If only curried-rice were so easy as curried-hanoi ;-).

-- Benjamin L. Russell

>On Thu, Oct 16, 2008 at 6:11 AM, Benjamin L. Russell
><DekuDekuplex at yahoo.com> wrote:
>> This time, I would like to write a type signature for a
>> multi-parameter function of a fixed number of arguments in Typed
>> Scheme, but the documentation ("Typed Scheme: Scheme with Static
>> Types" at http://docs.plt-scheme.org/typed-scheme/) is not clear on
>> this.
>>
>> I know how to write a type signature for a function of one argument;
>> e.g.:
>>
>> #lang typed-scheme
>>
>> (: fac (Number -> Number))
>> (define (fac n)
>>  (if (= n 0)
>>      1
>>      (* n (fac (- n 1)))))
>>
>>> (fac 5)
>> - : Number
>> 120
>>>
>>
>> I also know how to write a type signature for a function of zero
>> arguments; e.g.:
>>
>> #lang typed-scheme
>>
>> (: hello-world-function (-> Void))
>> (define (hello-world-function)
>>  (display "Hello, world!\n"))
>>
>>> (hello-world-function)
>> Hello, world!
>>>
>>
>> Additionally, I know how to write a type signature for a function of a
>> variable number of arguments:
>>
>> #lang typed-scheme
>>
>> (: my-plus-variable (Number * -> Number))
>> (define (my-plus-variable . ns)
>>  (if (null? ns)
>>      0
>>      (+ (car ns) (apply my-plus-variable (cdr ns)))))
>>
>>> (my-plus-variable)
>> - : Number
>> 0
>>> (my-plus-variable 1 2)
>> - : Number
>> 3
>>> (my-plus-variable 1 2 3)
>> - : Number
>> 6
>>>
>>
>> However, I don't know how to write a type signature for a function of
>> a fixed number n of arguments, where n > 1.  Here are my attempts to
>> write a function, my-plus, which takes exactly two arguments n1 and
>> n2, and returns their sum:
>>
>> #lang typed-scheme
>>
>> (: my-plus Number -> Number -> Number)
>> (define (my-plus n1 n2)
>>  (+ n1 n2))
>>
>> . <unsaved editor>:3:0: type declaration: too many arguments in: (:
>> my-plus Number -> Number -> Number)
>>
>> Here's another attempt:
>>
>> #lang typed-scheme
>>
>> (: my-plus (Number -> (Number -> Number)))
>> (define (my-plus n1 n2)
>>  (+ n1 n2))
>>
>> . <unsaved editor>:4:0: typecheck: Expected function with 1 argument,
>> but got function with 2 arguments in: (define (my-plus n1 n2) (+ n1
>> n2))
>> .
>>
>> I want to pass my-plus two separate arguments of type Number, n1 and
>> n2, and return their sum.  This is how my function is written in
>> regular #lang scheme:
>>
>> #lang scheme
>>
>> (define (my-plus n1 n2)
>>  (+ n1 n2))
>>
>>> (my-plus 1 2)
>> 3
>>>
>>
>> Can somebody please explain how I can write this function in Typed
>> Scheme?
>>
>> Also, does Typed Scheme support currying (from the results that I have
>> seen so far, apparently it doesn't)?
>>
>> -- Benjamin L. Russell