<div dir="ltr"><div class="markdown-here-wrapper" style><p style="margin:1.2em 0px!important">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:</p>
<pre style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;font-size:1em;line-height:1.2em;margin:1.2em 0px"><code style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);border-top-left-radius:3px;border-top-right-radius:3px;border-bottom-right-radius:3px;border-bottom-left-radius:3px;display:inline;background-color:rgb(248,248,248);white-space:pre;overflow:auto;border-top-left-radius:3px;border-top-right-radius:3px;border-bottom-right-radius:3px;border-bottom-left-radius:3px;border:1px solid rgb(204,204,204);padding:0.5em 0.7em;display:block!important">#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)
</code></pre><p style="margin:1.2em 0px!important">However, the typed form of this code gives a type error:</p>
<pre style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;font-size:1em;line-height:1.2em;margin:1.2em 0px"><code style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);border-top-left-radius:3px;border-top-right-radius:3px;border-bottom-right-radius:3px;border-bottom-left-radius:3px;display:inline;background-color:rgb(248,248,248);white-space:pre;overflow:auto;border-top-left-radius:3px;border-top-right-radius:3px;border-bottom-right-radius:3px;border-bottom-left-radius:3px;border:1px solid rgb(204,204,204);padding:0.5em 0.7em;display:block!important">#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)
</code></pre><p style="margin:1.2em 0px!important">Specifically, the type checker outputs:</p>
<pre style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;font-size:1em;line-height:1.2em;margin:1.2em 0px"><code style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);border-top-left-radius:3px;border-top-right-radius:3px;border-bottom-right-radius:3px;border-bottom-left-radius:3px;display:inline;background-color:rgb(248,248,248);white-space:pre;overflow:auto;border-top-left-radius:3px;border-top-right-radius:3px;border-bottom-right-radius:3px;border-bottom-left-radius:3px;border:1px solid rgb(204,204,204);padding:0.5em 0.7em;display:block!important">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)
</code></pre><p style="margin:1.2em 0px!important">I think the issue may be in that first line of the type definition, <code style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);border-top-left-radius:3px;border-top-right-radius:3px;border-bottom-right-radius:3px;border-bottom-left-radius:3px;display:inline;background-color:rgb(248,248,248)">(-> a b c d d) d (Listof a) (Listof b) (Listof d) -> d</code>. Shouldn’t that last argument type be <code style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);border-top-left-radius:3px;border-top-right-radius:3px;border-bottom-right-radius:3px;border-bottom-left-radius:3px;display:inline;background-color:rgb(248,248,248)">(Listof c)</code> instead of <code style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);border-top-left-radius:3px;border-top-right-radius:3px;border-bottom-right-radius:3px;border-bottom-left-radius:3px;display:inline;background-color:rgb(248,248,248)">(Listof d)</code>?</p>
<div title="MDH:SSB0aGluayB0aGVyZSBtYXkgYmUgYSBtaXN0YWtlIGluIHRoZSB0eXBlIGRlZmluaXRpb24gb2Yg
Zm9sZGwgZm9yIHRoZSBjYXNlIHRoYXQgYWNjZXB0cyBhbiBpbml0aWFsIHZhbHVlIGFuZCB0aHJl
ZSBsaXN0cyBhbmQgYSBmdW5jdGlvbiBvZiBmb3VyIHZhbHVlcyB0byBmb2xkIHRoZW0gb3Zlci4g
VGhlIGZvbGxvd2luZyB1bnR5cGVkIGNvZGUgcnVucyBjb3JyZWN0bHk6PGRpdj48YnI+PC9kaXY+
PGRpdj48ZGl2PiZuYnNwOyAmbmJzcDsgI2xhbmcgcmFja2V0PC9kaXY+PGRpdj4mbmJzcDsgJm5i
c3A7IChkZWZpbmUgKGYgYSBiIGMgZCkgZCk8L2Rpdj48ZGl2PiZuYnNwOyAmbmJzcDsgKGRlZmlu
ZSBucyAnKDAgMSAyKSk8L2Rpdj48ZGl2PiZuYnNwOyAmbmJzcDsgKGRlZmluZSB2cyAnKGEgMiAi
YiIpKTwvZGl2PjxkaXY+Jm5ic3A7ICZuYnNwOyAoZm9sZGwgZiAnb2sgbnMgbnMgdnMpPC9kaXY+
PC9kaXY+PGRpdj48YnI+PC9kaXY+PGRpdj5Ib3dldmVyLCB0aGUgdHlwZWQgZm9ybSBvZiB0aGlz
IGNvZGUgZ2l2ZXMgYSB0eXBlIGVycm9yOjwvZGl2PjxkaXY+PGJyPjwvZGl2PjxkaXY+PGRpdj4m
bmJzcDsgJm5ic3A7Jm5ic3A7I2xhbmcgdHlwZWQvcmFja2V0PC9kaXY+PGRpdj4mbmJzcDsgJm5i
c3A7Jm5ic3A7KGRlZmluZTogKGYgW2EgOiBOYXR1cmFsXSBbYiA6IE5hdHVyYWxdIFtjIDogQW55
XSBbZCA6IFN5bWJvbF0pIDogU3ltYm9sIGQpPC9kaXY+PGRpdj4mbmJzcDsgJm5ic3A7Jm5ic3A7
KDogbnMgKExpc3RvZiBOYXR1cmFsKSk8L2Rpdj48ZGl2PiZuYnNwOyAmbmJzcDsmbmJzcDsoZGVm
aW5lIG5zICcoMCAxIDIpKTwvZGl2PjxkaXY+Jm5ic3A7ICZuYnNwOyZuYnNwOyg6IHZzIChMaXN0
b2YgQW55KSk8L2Rpdj48ZGl2PiZuYnNwOyAmbmJzcDsmbmJzcDsoZGVmaW5lIHZzICcoYSAyICJi
IikpPC9kaXY+PGRpdj4mbmJzcDsgJm5ic3A7Jm5ic3A7KGZvbGRsIGYgJ29rIG5zIG5zIHZzKTwv
ZGl2PjwvZGl2PjxkaXY+PGJyPjwvZGl2PjxkaXY+U3BlY2lmaWNhbGx5LCB0aGUgdHlwZSBjaGVj
a2VyIG91dHB1dHM6PC9kaXY+PGRpdj48YnI+PC9kaXY+PGRpdj48ZGl2PiZuYnNwOyAmbmJzcDsm
bmJzcDtUeXBlIENoZWNrZXI6IFBvbHltb3JwaGljIGZ1bmN0aW9uIGBmb2xkbCcgY291bGQgbm90
IGJlIGFwcGxpZWQgdG8gYXJndW1lbnRzOjwvZGl2PjxkaXY+Jm5ic3A7ICZuYnNwOyZuYnNwO1R5
cGVzOiAoLSZndDsgYSBiIGMgZCBkKSBkIChMaXN0b2YgYSkgKExpc3RvZiBiKSAoTGlzdG9mIGQp
IC0mZ3Q7IGQ8L2Rpdj48ZGl2PiZuYnNwOyAmbmJzcDsmbmJzcDsmbmJzcDsgJm5ic3A7ICZuYnNw
OyAmbmJzcDsoLSZndDsgYSBiIGMgYykgYyAoTGlzdG9mIGEpIChMaXN0b2YgYikgLSZndDsgYzwv
ZGl2PjxkaXY+Jm5ic3A7ICZuYnNwOyZuYnNwOyZuYnNwOyAmbmJzcDsmbmJzcDsmbmJzcDsgJm5i
c3A7KC0mZ3Q7IGEgYiBiKSBiIChMaXN0b2YgYSkgLSZndDsgYjwvZGl2PjxkaXY+Jm5ic3A7ICZu
YnNwOyZuYnNwO0FyZ3VtZW50czogKC0mZ3Q7IE5vbm5lZ2F0aXZlLUludGVnZXIgTm9ubmVnYXRp
dmUtSW50ZWdlciBBbnkgU3ltYm9sIFN5bWJvbCkgJ29rIChMaXN0b2YgTm9ubmVnYXRpdmUtSW50
ZWdlcikgKExpc3RvZiBOb25uZWdhdGl2ZS1JbnRlZ2VyKSAoTGlzdG9mIEFueSk8L2Rpdj48ZGl2
PiZuYnNwOyAmbmJzcDsmbmJzcDtFeHBlY3RlZCByZXN1bHQ6IEFueVZhbHVlczwvZGl2PjxkaXY+
Jm5ic3A7ICZuYnNwOyZuYnNwOyZuYnNwO2luOiAoZm9sZGwgZiAocXVvdGUgb2spIG5zIG5zIHZz
KTwvZGl2PjwvZGl2PjxkaXY+PGJyPjwvZGl2PjxkaXY+SSB0aGluayB0aGUgaXNzdWUgbWF5IGJl
IGluIHRoYXQgZmlyc3QgbGluZSBvZiB0aGUgdHlwZSBkZWZpbml0aW9uLCBgKC0mZ3Q7IGEgYiBj
IGQgZCkgZCAoTGlzdG9mIGEpIChMaXN0b2YgYikgKExpc3RvZiBkKSAtJmd0OyBkYC4gU2hvdWxk
bid0IHRoYXQgbGFzdCBhcmd1bWVudCB0eXBlIGJlIGAoTGlzdG9mIGMpYCBpbnN0ZWFkIG9mIGAo
TGlzdG9mIGQpYD88L2Rpdj4=" style="height:0;font-size:0em;padding:0;margin:0">​</div></div></div>