Open RobertHarper opened 8 years ago
Regarding your last paragraph, it'd indeed be nice to be able to recover the final value of a suspension by pattern matching, as it would eliminate the verbosity of explicitly calling a Lazy.force
function (or whatever its name is), e.g.
case whatever of
Foo (!a,!b,!c) => ... a ... b ... c ...
| Bar (!x,!y,!z) => ... x ... y ... z ...
Instead of:
case whatever of
Foo (a,b,c) => ... Lazy.force a ... Lazy.force b ... Lazy.force c ...
| Bar (x,y,z) => ... Lazy.force x ... Lazy.force y ... Lazy.force z ...
I'd go even further, and suggests that Successor ML add view patterns, so that arbitrary abstract data types can be pattern-matched against, not just suspensions.
FYI: SML/NJ implements lazy datatypes and patterns following the design by Wadler, Taha, and MacQueen.
What I don't like so much about SML/NJ's datatype lazy
feature is that it doesn't give me fine-grained enough control over where I'm using suspensions in my program, since they always come bundled with datatype lazy
constructors. There's no concrete benefit to this bundling, unlike, say, bundlingdatatype
s with recursive types, which aids type inference. I'd much rather have an abstract type of suspensions, which I can use whenever I want (e.g., the second component of a triplet can be suspended, without having to declare a separate datatype lazy
), although an obvious deficiency of my implementation is that it isn't thread-safe.
I would agree. Laziness is not a property of a datatype, it’s a concept of its own. I suggested in my MLW talk a syntax for doing this in a reasonably lightweight way.
Bob
On Jun 30, 2016, at 16:10, eduardoleon notifications@github.com wrote:
What I don't like so much about SML/NJ's datatype lazy feature is that it doesn't give me fine-grained enough control over where I'm using suspensions in my program, since they always come bundled with datatype lazy constructors. I'd much rather have an abstract type of suspensions https://github.com/eduardoleon/typhoon/blob/master/Lazy.sml, which I can use whenever https://github.com/eduardoleon/typhoon/blob/master/Seq.Queue.sml I want https://github.com/eduardoleon/typhoon/blob/master/Seq.Catenable.sml, although an obvious deficiency of my implementation is that it isn't thread-safe.
— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/SMLFamily/Successor-ML/issues/17#issuecomment-229773808, or mute the thread https://github.com/notifications/unsubscribe/ABdsdYW1-wd8Sj18O40y6uNBvBdExEnuks5qRCKYgaJpZM4IDt5W.
Just like we have both fun
(for declarations) and fn
(for expressions), we should have both declarations and expressions for need cells. Something like nd => (* ... *)
or nd (* ... *)
would work.
I don't understand the desire to rely on pattern-matching to force a need cell. Why not just retrieve a need cell's contents with a simple operator, something like !!cell
. We could also allow pattern-matching as an alternative way of extracting a need cell's value using val (lazy x) = cell
, just like how you can apparently do val (ref x) = r
. But does anyone actually use ref
like that? I didn't even know you could until I was reading about the value restriction and saw that ref
was a constructor and not a function.
As an example of a pure extension to the language (one that does not break old code), we should certainly consider adding laziness. Wadler's proposal is probably a good starting point; there have been others.
The simplest is probably to introduce need bindings, which must be permitted to be (mutually) recursive. So we should be able to write something like the declaration need x = e where x has type tau susp if e has type tau. For the self-referential case, it would be need rec x = e, where now e has type tau under the supposition that x has type tau susp; the result is a tau susp. As usual, rec would have to distribute over and so that mutually recursive need cells are possible.
Then forcing suspensions would be integrated into pattern matching. Some sort of notation would be needed (ahem), for example !p in a pattern to indicate that the corresponding value is to be forced and its value matched against p, which could be an as or with pattern. There would need to be a clear sequential semantics for pattern matching so that it is clear what is forced when. As long as expressions can be impure, it is visible when things are forced and we cannot leave that undefined.