Re: [Haskell-cafe] If you'd design a Haskell-like language, what would you do different?

On 22 Dec 2011, at 21:29, MigMit wrote:

Отправлено с iPad

22.12.2011, в 23:56, Conor McBride написал(а):

...

I'd be glad if "pure" meant "total", but partiality were an effect supported by the run-time system. Then we could choose to restrict ourselves, but we wouldn't be restricted by the language.

I second that. Having a special "partiality" monad would be nice. However, I'm not certain as to how it would interact with recursion — if f is a total function, fix f could be (and almost certainly would be) a possibly undiefined value. So, fix should have type "(a -

...

a) -> Partial a"; that's OK, but implicit uses of fix (I mean let statements) would be quite different.

Indeed they would, at least to the extent of making clear in the type on what basis recursive calls should be checked.

...

I'd like to program with an applicative notion, but in monadic types. That's what I'd do different, and for me, the subject is not a hypothetical question.

So... you are developing a programming language with all calculations being automatically lifted to a monad? What if we want to do calculations with monadic values themselves, like, for example, store a few monadic calculations in a list (without joining all there effects as the sequence function does)?

The plan is to make a clearer distinction between "being" and "doing" by splitting types clearly into an effect part and a value part, in a sort of a Levy-style call-by-push-value way. The notation [<list of effects>]<value type> is a computation type whose inhabitants might *do* some of the effects in order to produce a value which *is* of the given value type. But it is always possible to make a value type from a computation type by suspending it (with braces), so that {[<list of effects>]<value type>} is a value type for suspended computations, which *are* things which one could potentially *do* at another time. But we can manipulate suspended computations purely. Haskell doesn't draw a clear line in types between the effect part and the value part, or support easy fluidity of shifting roles between the two. Rather we have two modes: (1) the implicit partiality mode, where the value part is the whole of the type and the notation is applicative; (2) the explicit side-effect mode, where the type is an effect operator applied to the value type and the notation is imperative. It's an awkward split, and it makes it tricky to make clean local renegotiations of effectful capabilities by hiding or handling them. Also, I don't see why partiality deserves an applicative notation where other, perhaps more benign effects (like *handled* exceptions) are forced into an imperative (or clunky Applicative) mode. Maybe this strays too far to classify as "Haskell-like", but it's an attempt to re-rationalise techniques that emerged from Haskell programming. Cheers Conor