[MLton] Bug in signature ascription
Vesa Karvonen
vesa.karvonen at cs.helsinki.fi
Wed Feb 7 01:59:25 PST 2007
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
More information about the MLton
mailing list