[MLton] Bug in signature ascription

[Vesa Karvonen]

Quoting "Wesley W. Terpstra" <terpstra at gkec.tu-darmstadt.de>:
[...]
> Let me confirm that I understand what you're saying: Foldr needs  
> enough polymorphism to match the signature FOLD. Unfortunately, the  
> implementation of Foldr required more polymorphism from Fold than  
> FOLD let escape. That's quite a nasty corner case, and I would've  
> never suspected it. Thanks! I just assumed that Vesa's signature was  
> correct since the whole Fold structure is deep magic that I'm  
> terrified to touch. :-)
> 
> In fact, I've already found that Foldr.t needs five type variables,  
> or it breaks variable arity polymorphism. So, I guess the wiki page  
> which describes the signature is wrong. I'll correct the page as soon  
> as I've found the polymorphism that Fold lost.

The Wiki page (http://mlton.org/Fold) is by Stephen.  I did some work
on the Fold technique and you can find the code at:
  http://www.cs.helsinki.fi/u/vkarvone/fold/ .
I promised to update the Wiki pages, but I haven't yet found the time.

It has been a while since I last worked on Fold stuff.  I think that
the FOLD signature for the Fold structure is "correct" and general
enough (although it is not the principal signature).  As you noticed,
I think Foldr (as it stands) needs a different signature.  Note that
Fold evaluates steps (applies the step function to the carried state)
immediately while Foldr delays them to the end.

I believe I designed FoldFnL and FoldFnR structures in an attempt to
make them more alike:

  http://www.cs.helsinki.fi/u/vkarvone/fold/foldfn.sml .

Here is the code for reference:

structure FoldFnL =
  struct
    fun fold d = Fold.fold (id, d)
    fun step0 f = Fold.step0 (fn g => f o g)
    fun step1 f = Fold.step1 (fn (x, g) => f x o g)
  end

structure FoldFnR =
  struct
    fun fold d = Fold.fold (id, d)
    fun step0 f = Fold.step0 (fn g => g o f)
    fun step1 f = Fold.step1 (fn (x, g) => g o f x)
  end

>From the above, SML/NJ gives:

structure FoldFnL :
  sig
    val fold : ('a -> 'b) -> ('c -> 'c,'a,'b,'d) Fold.t
    val step0 : ('a -> 'b) -> ('c -> 'a,'c -> 'b,'d,'e,'f) Fold.step0
    val step1 : ('a -> 'b -> 'c) -> ('a,'d -> 'b,'d -> 'c,'e,'f,'g) Fold.step1
  end

structure FoldFnR :
  sig
    val fold : ('a -> 'b) -> ('c -> 'c,'a,'b,'d) Fold.t
    val step0 : ('a -> 'b) -> ('b -> 'c,'a -> 'c,'d,'e,'f) Fold.step0
    val step1 : ('a -> 'b -> 'c) -> ('a,'c -> 'd,'b -> 'd,'e,'f,'g) Fold.step1
  end

As you can see, the inferred signatures are very similar except
that arrows are reversed.

-Vesa Karvonen