I'm sure we've all used the Writer monad from time to time when we want to yield a value which will propagate up several levels of a recursive call tree "behind the scenes". And we've all been annoyed at having to rewrite the whole function in monadic style. WriterT is less intrusive, but not much so, since we have to pepper the code with calls to "lift". I think there's a better solution. It should be possible to turn the idea of linear implicit parameters upside-down, to get values which are automatically propagated upwards and merged as necessary. We would need a class "Mergeable", a counterpart to "Splittable". But we already have such a class (Monoid). Here's a possible syntax. An expression like (123, ^x = "foo") would have the type (Integer, ^x :: String), which is like a tuple but with all but one of the elements having a name. An expression like (123, ^x="foo") - (45, ^x="bar", ^y="baz") would be converted by the compiler to (123 - 45, ^x=("foo" `mappend` "bar"), ^y="baz"), even if the two values passed to (-) were returned from a recursive call and not written out explicitly as I've done here. These return values could then be extracted by matching against the pattern (a, ^x = b), which would return the value of ^x in b, and the scrutinee with ^x removed in a. The semantics seems very simple -- virtually identical to implicit parameters. Implicit return values are dual to exceptions-as-values in some sense: they use an implicit product return type instead of a sum. It should be possible to implicitly return values which are not instances of Monoid: the compiler errors out if it ever needs to merge such a type. Wouldn't this provide a form of uniqueness typing a la Clean? In fact, couldn't we implement safe state threads on top of this, instead of the ST monad? In fact, couldn't we work within several state threads at once? -- Ben
Alle 00:57, lunedì 26 gennaio 2004, Ben Rudiak-Gould ha scritto:
Here's a possible syntax. An expression like (123, ^x = "foo") would have the type (Integer, ^x :: String), which is like a tuple but with all but one of the elements having a name. An expression like
(123, ^x="foo") - (45, ^x="bar", ^y="baz")
would be converted by the compiler to
(123 - 45, ^x=("foo" `mappend` "bar"), ^y="baz")
It's unclear to me how would the compiler know that it's not (123 - 45, ^x=("bar" `mappend` "foo"), ^y="baz") This depends on order of evaluation or am I wrong? V. -- A: Top posting! Q: What is the most irritating thing on Usenet?
On Mon, 26 Jan 2004, Vincenzo aka Nick Name wrote:
Alle 00:57, luned� 26 gennaio 2004, Ben Rudiak-Gould ha scritto:
(123, ^x="foo") - (45, ^x="bar", ^y="baz")
would be converted by the compiler to
(123 - 45, ^x=("foo" `mappend` "bar"), ^y="baz")
It's unclear to me how would the compiler know that it's not
(123 - 45, ^x=("bar" `mappend` "foo"), ^y="baz")
This depends on order of evaluation or am I wrong?
No, it depends only on the order of the source code. The value on the left of the mappend is the value that's leftmost in the original expression. -- Ben
I wrote:
It should be possible to implicitly return values which are not instances of Monoid: the compiler errors out if it ever needs to merge such a type. Wouldn't this provide a form of uniqueness typing a la Clean? In fact, couldn't we implement safe state threads on top of this, instead of the ST monad? In fact, couldn't we work within several state threads at once?
I think the answer is yes: I think this idea can replace the IO, ST and State monads and provide a much finer-grained form of ordering, and easy mixing. We add a new sequencing construct to Haskell, along the lines of do and proc. I'll call it "thread", though this is probably a poor choice. It takes a list of expressions and causes the implicit return values of each expression except the last one to be passed as implicit parameters to the next expression in the list. Implicit parameters not "consumed" by a particular expression would have to become implicit return values, and I'm not sure exactly how this should work. The main function has a type like (?io :: State) => ((), ^io :: State) The state parameter must be unforgeable. The simplest way to achieve this is to give it a special name which the program is forbidden to mention in binding and pattern-matching constructs. Of course this threading carries no runtime cost, as the code generator knows not to generate code to pass values of type State around. Each time the user creates a ref (or mutable array), it gets its own independent state parameter, which is automatically threaded through future uses of the ref by "thread" constructs. Any function that uses certain refs will include in its type an explicit list of the associated state parameters of those refs. This creates a problem: if each ref has its own state parameter, what are their names? This issue came up with implicit parameters also: the fact that implicit parameters have only names, whereas typeclasses are parameterized by type, was a source of surprising differences between the two. I see now that this can be solved by allowing implicit parameters and return values to be parameterized by types as well. Thus we have newRef :: a -> (exists s . Ref s a, ^st s :: State) readRef :: (?st s :: State) => Ref s a -> (a, ^st s :: State) writeRef :: (?st s :: State) => Ref s a -> a -> ((), ^st s :: State) (It's not clear that readRef actually needs to return the state.) Furthermore, there should be a subclassing system for implicit values, so that (for example) the IO monad can be split into independent pieces and ?io can be shorthand for all of them. -- Ben
I wrote:
newRef :: a -> (exists s . Ref s a, ^st s :: State) readRef :: (?st s :: State) => Ref s a -> (a, ^st s :: State) writeRef :: (?st s :: State) => Ref s a -> a -> ((), ^st s :: State)
(It's not clear that readRef actually needs to return the state.)
It shouldn't, and neither should writeRef need to *take* the state. And the type a should be moved from the ref to the state parameter. I think this gives us statically safe polymorphic refs. And I forgot some parentheses in newRef. I think these are the right types: newRef :: a -> (exists s . (Ref s, ^st s a :: State)) readRef :: (?st s a :: State) => Ref s -> a writeRef :: Ref s -> a -> ((), ^st s a :: State) -- Ben
On Sun, 25 Jan 2004, David Bergman wrote:
Ben, it seems that you are having a quite fruitful discussion with yourself ;-)
Anyone who wants to join in is welcome. :-)
I will just wait here for a more conclusive form of your backward-propagating linear parameter.
I'm not changing the idea, just extending it (and making minor corrections). I stand by the original article as much as I ever did. Apologies for flooding the list, but I think I'll be done soon. Just one tiny little addition... -- Ben
Continuing my one-sided discussion:
newRef :: a -> (exists s . (Ref s, ^st s a :: State)) readRef :: (?st s a :: State) => Ref s -> a writeRef :: Ref s -> a -> ((), ^st s a :: State)
?io and ?st should have been %io and %st, of course. It's essential that these be linear (and that State is not an instance of Splittable). It might also be useful to have this function: anotherRef :: (%st s :: State) => Ref s a -> a -> (Ref s a, ^st s :: State) which creates a new ref in the same state space as an old one. However, this requires that the "a" parameter be moved back to the Ref, if we want the new ref to have an independent type. So there seem to be two kinds of refs, serially-typed and parallel-typed, which can't share the same state space (though they can be mixed in a single thread construct). Another minor point: in case it wasn't clear, it should be possible to write a type synonym like type IO a = (%io :: State) => (a, ^io :: State) after which main would have the type IO (), as always. -- Ben
participants (3)
-
Ben Rudiak-Gould -
David Bergman -
Vincenzo aka Nick Name