[racket] Possible issue in the typed version of foldl

From: Jack Firth (jackhfirth at gmail.com)
Date: Mon Oct 20 02:16:11 EDT 2014

I think there may be a mistake in the type definition of foldl for the case
that accepts an initial value and three lists and a function of four values
to fold them over. The following untyped code runs correctly:

#lang racket
(define (f a b c d) d)
(define ns '(0 1 2))
(define vs '(a 2 "b"))
(foldl f 'ok ns ns vs)

However, the typed form of this code gives a type error:

#lang typed/racket
(define: (f [a : Natural] [b : Natural] [c : Any] [d : Symbol]) : Symbol d)
(: ns (Listof Natural))
(define ns '(0 1 2))
(: vs (Listof Any))
(define vs '(a 2 "b"))
(foldl f 'ok ns ns vs)

Specifically, the type checker outputs:

Type Checker: Polymorphic function `foldl' could not be applied to arguments:
Types: (-> a b c d d) d (Listof a) (Listof b) (Listof d) -> d
       (-> a b c c) c (Listof a) (Listof b) -> c
       (-> a b b) b (Listof a) -> b
Arguments: (-> Nonnegative-Integer Nonnegative-Integer Any Symbol
Symbol) 'ok (Listof Nonnegative-Integer) (Listof Nonnegative-Integer)
(Listof Any)
Expected result: AnyValues
 in: (foldl f (quote ok) ns ns vs)

I think the issue may be in that first line of the type definition, (-> a b
c d d) d (Listof a) (Listof b) (Listof d) -> d. Shouldn’t that last
argument type be (Listof c) instead of (Listof d)?
​
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20141019/4903055a/attachment.html>

Posted on the users mailing list.