* Alexander Solla [2011-12-19 19:10:32-0800]

* Documentation that discourages thinking about bottom as a 'value'. It's not a value, and that is what defines it.

In denotational semantics, every well-formed term in the language must have a value. So, what is a value of "fix id"? -- Roman I. Cheplyaka :: http://ro-che.info/

How would you represent it then? Would it cause a compiler error? Thiago. 2011/12/20 Ben Lippmeier :

On 20/12/2011, at 6:06 PM, Roman Cheplyaka wrote:

...

* Alexander Solla [2011-12-19 19:10:32-0800]

...

* Documentation that discourages thinking about bottom as a 'value'.  It's not a value, and that is what defines it.

In denotational semantics, every well-formed term in the language must have a value. So, what is a value of "fix id"?

There isn't one!

Bottoms will be the null pointers of the 2010's, you watch.

Ben.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Tue, Dec 20, 2011 at 8:46 PM, Ben Lippmeier wrote:

On 20/12/2011, at 6:06 PM, Roman Cheplyaka wrote:

...

* Alexander Solla [2011-12-19 19:10:32-0800]

...

* Documentation that discourages thinking about bottom as a 'value'. It's not a value, and that is what defines it.

In denotational semantics, every well-formed term in the language must have a value. So, what is a value of "fix id"?

There isn't one!

Bottoms will be the null pointers of the 2010's, you watch.

This ×1000. Errors go in an error monad.

Ben.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

...

...

In denotational semantics, every well-formed term in the language must have a value. So, what is a value of "fix id"?

There isn't one!

Bottoms will be the null pointers of the 2010's, you watch.

This ×1000. Errors go in an error monad.

Including all possible manifestations of infinite loops?

Some would say that non-termination is a computational effect, and I can argue either way depending on the day of the week. Of course, the history books show that monads were invented *after* it was decided that Haskell would be a lazy language. Talk about selection bias. Ben.

On 20/12/2011, at 21:52 , Gregory Crosswhite wrote:

...

Some would say that non-termination is a computational effect, and I can argue either way depending on the day of the week.

*shrug* I figure that whether you call _|_ a value is like whether you accept the Axiom of Choice: it is a situational decision that depends on what you are trying to learn more about.

I agree, but I'd like to have more control over my situation. Right now we have boxed and lifted Int, and unboxed and unlifted Int#, but not the boxed and unlifted version, which IMO is usually what you want.

...

Of course, the history books show that monads were invented *after* it was decided that Haskell would be a lazy language. Talk about selection bias.

True, but I am not quite sure how that is relevant to _|_...

I meant to address the implicit question "why doesn't Haskell use monads to describe non-termination already". The answer isn't necessarily "because it's not a good idea", it's because "that wasn't an option at the time".

Dec 20, 2011, в 14:40, Jesse Schalken написал(а):

...

Including all possible manifestations of infinite loops?

So... this imaginary language of yours would be able to solve the halting problem?

All type systems are incomplete. The idea is to do a termination analysis, and if the program can not be proved to terminate, then it is marked as "possibly non-terminating". This isn't the same as deciding something is "*definitely* non-terminating", which is what the halting problem is about. This "possibly non-terminating" approach is already used by Coq, Agda and other languages. Ben.

On Dec 20, 2011, at 8:40 PM, Jesse Schalken wrote:

If you think a value might not reduce, return an error in an error monad.

Okay, I'm completely convinced! Now all that we have to do is to solve the halting problem to make your solution work... :-) Cheers, Greg

On Dec 20, 2011, at 9:18 PM, Jesse Schalken wrote:

Why do you have to solve the halting problem?

You have to solve the halting problem if you want to replace every place where _|_ could occur with an Error monad (or something similar), because _|_ includes occasions when functions will never terminate.

Consider integer division by 0. [...] This is all I was talking about.

But imagine there was an occasion where you *knew* that the divisor was never zero --- say, because the divisor was constructed to be a natural number. Now there is no point in running in the Error monad because there will never such a runtime error; in fact, it is not clear what you would even *do* with a Left value anyway, short of terminating the program and printing and error, which is what would have happened anyway. Furthermore, it is easy to imagine circumstances where you have now forced your entire program to run in the Error monad, which makes everything incredibly inconvenient with no benefit at all. This is the problem with arguments against partial functions; they don't solve any problems at all except in the case where you have untrusted data in which case you should be using a different function or manually checking it anyway, and they add a lot of wasted overhead. Cheers, Greg

What I think to be the hard part to do is to put this on the type system, e.g.: intDiv x y = if y > x then 0 else 1 + (intDiv (x - y) y) Should not compile. Otherwise you will need the bottom value. Am I missing something? Thiago. 2011/12/20 Jesse Schalken :

On Tue, Dec 20, 2011 at 10:43 PM, Gregory Crosswhite wrote:

...

On Dec 20, 2011, at 9:18 PM, Jesse Schalken wrote:

Why do you have to solve the halting problem?

You have to solve the halting problem if you want to replace every place where _|_ could occur with an Error monad (or something similar), because _|_ includes occasions when functions will never terminate.

I think we're talking about different things. By "bottom" I mean the function explicitly returns "error ..." or "undefined". In those cases, it should go in an error monad instead. In cases where there is an infinite loop, the function doesn't return anything because it never finishes, and indeed this separate problem will never be solved while remaining Turing complete because it is the halting problem.

...

Consider integer division by 0.  [...] This is all I was talking about.

But imagine there was an occasion where you *knew* that the divisor was never zero --- say, because the divisor was constructed to be a natural number.

Then use a separate type for natural numbers excluding 0. Then you can define a total integer division function on it (although the return value may be zero and so needs a different type).

...

Now there is no point in running in the Error monad because there will never such a runtime error;  in fact, it is not clear what you would even *do* with a Left value anyway, short of terminating the program and printing and error, which is what would have happened anyway.

What you do with a Left value is up to you - that's the point, you now have a choice. In fact, the value might not even be being handled by you, in which case someone else now has a choice.  Handling of the error is done in the same place as handling of the result, no IO needed.

...

Furthermore, it is easy to imagine circumstances where you have now forced your entire program to run in the Error monad, which makes everything incredibly inconvenient with no benefit at all.

This "inconvenience" I imagine is the extra code required to compose functions which return values in a monad as opposed to straight values. To me this is a small price to pay for knowing my code won't randomly crash, and I would rather this be handled syntactically to make composing monadic values more concise.

The point is your program shouldn't be able to make assumptions about values without proving them with types. It's often easier not to make the assumption and propagate some error in an error monad instead, but that's better than getting away with the assumption and having the program crash or behave erratically because the assumption turned out false.

...

This is the problem with arguments against partial functions;  they don't solve any problems at all except in the case where you have untrusted data in which case you should be using a different function or manually checking it anyway, and they add a lot of wasted overhead.

The whole term "untrusted data" baffles me. How often can you actually "trust" your data? When you send your software out into the wild, what assumptions can you make about its input? What assumptions can you make about the input to a small part of a larger program which is millions of lines? You can often deduce that certain values do/do not occur in small parts of code, but the difficulty of such deductions increases exponentially with the size of the codebase, and is a job done much better by a type system.

Also I would like to think this "wasted overhead" can be optimised away at some stage of compilation, or somehow removed without the programmer needing to think about it. Maybe I'm just dreaming on those fronts, however.

...

Cheers, Greg

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Wed, Dec 21, 2011 at 1:09 AM, Gregory Crosswhite wrote:

On Dec 20, 2011, at 11:21 PM, Jesse Schalken wrote:

On Tue, Dec 20, 2011 at 10:43 PM, Gregory Crosswhite < gcrosswhite@gmail.com> wrote:

...

On Dec 20, 2011, at 9:18 PM, Jesse Schalken wrote:

Why do you have to solve the halting problem?

You have to solve the halting problem if you want to replace every place where _|_ could occur with an Error monad (or something similar), because _|_ includes occasions when functions will never terminate.

I think we're talking about different things. By "bottom" I mean the function explicitly returns "error ..." or "undefined". In those cases, it should go in an error monad instead. In cases where there is an infinite loop, the function doesn't return anything because it never finishes, and indeed this separate problem will never be solved while remaining Turing complete because it is the halting problem.

Then honestly you should choose a different term because I am pretty certain that my use of the term "bottom" is the commonly accepted one which (among other places) appears in denotation semantics.

I apologize if I was using the wrong terminology. I've seen "error ..." shown as, and understood it to be, _|_, but it seems _|_ refers to either a value that does not reduce or Haskell's "error" function depending on the context.

...

Consider integer division by 0. [...] This is all I was talking about.

But imagine there was an occasion where you *knew* that the divisor was never zero --- say, because the divisor was constructed to be a natural number.

Then use a separate type for natural numbers excluding 0. Then you can define a total integer division function on it (although the return value may be zero and so needs a different type).

That would certainly be a lovely idea *if* we were programming in Agda, but I was under the assumption that this conversation was about Haskell. :-)

I don't have experience with proof assistants, but maybe my answer to this thread can be summed up as giving Haskell that kind of capability. ;)

...

Now there is no point in running in the Error monad because there will never such a runtime error; in fact, it is not clear what you would even *do* with a Left value anyway, short of terminating the program and printing and error, which is what would have happened anyway.

What you do with a Left value is up to you - that's the point, you now have a choice.

Yes, but it is a pointless choice because if you had any reason to believe that your value was an invalid input to a function you would have checked it by now or used an alternative non-partial function that did run in an Error monad for that specific purpose.

In fact, the value might not even be being handled by you, in which case someone else now has a choice. Handling of the error is done in the same place as handling of the result, no IO needed.

Yes, but all that the user of your library knows at this point is that there is a bug somewhere in your library that violated an invariant. Nearly all of the time there is no way to recover from this in a useful way and so all the user will end up doing in response to your Left value is to abort anyway.

What if for example the program is a server which is always running. If you use "error ...", the server will crash, and someone has to go start it up again. The person who wrote the server has to remember to wrap each request in a try...catch block in the IO monad in the outer layer to make sure the server doesn't crash due to errors in pure code. What if they forget? If you use an error monad, they can't forget, because the type system forces them to handle the error. Maybe they will choose to "exit" in the case of an error, but at least then the program is crashing because they've explicitly told it to rather than because they forgot something. More likely they will respond to the request with an "error" response, allowing the server to continue running, but either way the type system has forced them to make a decision.

The point is your program shouldn't be able to make assumptions about values without proving them with types.

I agree but, again, we aren't talking about Agda here, we are talking about Haskell. :-)

Now I really want to look at proof assistants!

The whole term "untrusted data" baffles me. How often can you actually "trust" your data?

All the time! For example, if I create a counter that starts at 1, only increase it, and give nobody else access to it, then I can be as certain as it is possible to be can be that it is not 0.

Start your counter at 0 then. Then if you really don't want to deal with 0, treat 0 as 1 and 1 as 2 etc - hence a type for non-zero naturals. I think structuring code such that the types you use contain no useless or impossible values is often easy with a little thought, and worth it because the compiler is now verifying the assumptions you made. In cases where that isn't possible (or you can't be bothered), I'd rather just propagate an error in a monad than resort to Haskell's "error ..." for above reasons.

Also, there are occasionally times when I essentially check that a Maybe value is Just in one part of the code, and then in another part of the code need to extract the value from the Just; in such cases there is no point in using method *other* than simply fromJust to extract the value.

If you checked that a Maybe is a Just, then continued to pass on the Maybe to a function which assumed it is Just, then you should have just passed on the value in the Just instead. If it's Maybe, you must handle Nothing. If you've already handled Nothing, it doesn't make sense to keep dealing with a Maybe.

(Of course, it would be better to have condensed all of this into a single case statement in the first place, but sometimes --- say, when interfacing with others' libraries --- this ends up not being an available option.)

When you send your software out into the wild, what assumptions can you make about its input?

None, which is why in that case you need to test your input in that case.

Also I would like to think this "wasted overhead" can be optimised away at some stage of compilation, or somehow removed without the programmer needing to think about it.

I was thinking in terms of overhead from the coder's point of view, not from the compiler's point of view.

Cheers, Greg

On Dec 21, 2011, at 8:52 AM, Jesse Schalken wrote:

I don't have experience with proof assistants, but maybe my answer to this thread can be summed up as giving Haskell that kind of capability. ;)

Okay, then suffice it to say that most of what you said *is* implemented in real languages like Coq and Agda so you should check them out. :-) Unfortunately there are two hurdles one faces when using these languages: first, it is often very cumbersome to actually prove all of the invariants you want to prove to make your code total, and second, there is not yet a nice way of doing I/O actions and/or interfacing with external libraries written in other languages. However, until we have solved the problems that make working entirely in dependently-typed languages a pain, we will need to stick with languages with weaker type systems like Haskell, which means that we can't get around _|_ since we cannot encode all of our invariants into the type system. Incidentally, I would highly recommend learning more about Coq and Agda. There is a great textbook to start from available here: http://adam.chlipala.net/cpdt/ It is valuable because it is not Coq-specific but rather is a good general introduction to, exactly as the title promises, certified programming with dependent types. You should also really check out Agda; the main difference between it and Coq is the language in which proofs are written. To make a long story short, in Coq proofs are often easier to write because they use a specialized language for that purpose but this often makes them a bit of a black box, whereas in Agda the proofs are fully explicit which makes them much more transparent but also more verbose and often harder to write. Unfortunately the documentation for Agda tends to be sparse and split over several kinds of documents (such as theses, papers, etc.) so isn't an obvious guide for me to recommend to you, but if you look around you should find enough information to get you started. The home page is http://wiki.portal.chalmers.se/agda/pmwiki.php For me part of the most exciting part was reading through the Agda standard libraries, which you can download from http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary Just reading through their code is enlightening because it shows you just how much power is available from dependent types; the standard library also covers a lot more than Coq's does. Unfortunately it also showcases one of the limitations of Agda, which is things can often get cryptic and arcane very quickly, especially since Agda makes you work with "universes" explicitly (Coq handles them implicitly) which adds another layer of complexity. :-) (FYI, the universes are a hierarchy such that values are at the bottom, types of values one rung up, types of types two rungs up, types of types of types three rungs up, etc. Haskell is limited in only having a three-level hierarchy, with values, types, and kinds.) Cheers, Greg

MigMit wrote:

Dec 20, 2011, в 14:40, Jesse Schalken написал(а):

...

If you think a value might not reduce, return an error in an error monad. Then the caller is forced to handle the case of an error, or propagate the error upwards. The error can also be handled in pure code this way, whereas bottom can only be handled within the IO monad.

So... this imaginary language of yours would be able to solve the halting problem?

Depends on what you mean "solve" the halting problem. Agda and Coq are two languages that will only compile programs that can be proven to terminate. Non terminating programs are rejected. Erik -- ---------------------------------------------------------------------- Erik de Castro Lopo http://www.mega-nerd.com/

On 21 Dec 2011, at 08:24, Alexander Solla wrote:

I would rather have an incomplete semantic, and have all the incomplete parts collapsed into something we call "bottom".

I don't see the reason to limit ourselves to that. Of course, in total languages like Agda there is no need for (_|_). But in a turing-complete lazy language like Haskell we really need it. Of course, it makes not much sense to write "fix id" anywhere in your program; but, for example, lists like "1:2:3:4:5:_|_" can be really useful. And denotational semantics is not just nice. It is useful. It's the best way to understand why the program we just wrote doesn't terminate.

On Dec 22, 2011, at 12:25 PM, Alexander Solla wrote:

It is not "limiting" to make distinctions that capture real differences. An overly broad generalization limits what can be proved. Can we prove that every vehicle with wheels has a motor? Of course not -- bicycles exist. Can we prove every car has a motor? Yes we can. Throwing bottoms into the collection of values is like throwing bicycles into the collection of cars. We can say /less/ about the collection than we could before, /because/ the collection is more general.

Sure, throwing bottom into the set of values means that we can no longer prove as many nice properties about them. However, since bottom *does* exist in this set since functions cannot be guaranteed to terminate, the properties that we do prove will have more relevance. Cheers, Greg

On Wed, Dec 21, 2011 at 8:39 PM, MigMit wrote:

On 22 Dec 2011, at 06:25, Alexander Solla wrote:

...

Denotational semantics is unrealistic.

And so are imaginary numbers. But they are damn useful for electrical circuits calculations, so who cares?

Not a fair comparison. Quaternions are not particularly useful for electrical circuits, because it is unrealistic to apply a four-dimensional construct to two-dimensional phase spaces. In the same way, denotational semantics adds features which do not apply to a theory of finite computation.

...

The /defining/ feature of a bottom is that it doesn't have an interpretation.

What do you mean by "interpretation"?

You know, the basic notion of a function which maps syntax to concrete values. http://en.wikipedia.org/wiki/Model_theory

...

They should all be treated alike, and be treated differently from every other Haskell value.

But they ARE very similar to other values. They can be members of otherwise meaningful structures, and you can do calculations with these structures. "fst (1, _|_)" is a good and meaningful calculation.

Mere syntax. What is fst doing? It computes "forall (x,y) |- x". Using the language of model theory, we can say that Haskell computes an interpretation "forall (x,y) |= x". It is _|_ that lacks an intepretation, not fst. We can see that by trying "fst (_|_,1), which reduces to _|_ by the proof rule for fst. _|_ lacks an interpretation, so the run-time either loops forever or throws an error (notice that error throwing is only done with compiler magic -- if you define your own undefined = undefined, using it will loop. GHC is specially trained to look for Prelude.undefined to throw the "undefined" error.)

...

Every other Haskell value /does/ have an interpretation.

So, (_|_) is bad, but (1, _|_) is good?

I did not introduce "good" and "bad" into this discussion. I have merely said (in more words) that I want my hypothetical perfect language to prefer OPERATIONAL (model) SEMANTICS for a typed PARACONSISTENT LOGIC over the DENOTATIONAL SEMANTICS which the official documentation sometimes dips into. Using examples from denotational semantics is not going to change my mind about the applicability of one or the other. It is clear that denotational semantics is a Platonic model of constructive computation.

You know, my scientific advisor used to say "math is about calling different things by the same name; philosophy is about calling the same thing by different names". It seems to me that philosophy is something you're doing now, whereas programming is all about math.

Then you are mistaken. I am talking about choosing the appropriate mathematical model of computation to accurately, clearly, and simply describe the language's semantics.

Отправлено с iPad 24.12.2011, в 18:50, Alexander Solla написал(а):

In the same way, denotational semantics adds features which do not apply to a theory of finite computation.

And why exactly should we limit ourselves to some theory you happen to like?

...

The /defining/ feature of a bottom is that it doesn't have an interpretation.

What do you mean by "interpretation"?

You know, the basic notion of a function which maps syntax to concrete values.

http://en.wikipedia.org/wiki/Model_theory

But (_|_) IS a concrete value.

But they ARE very similar to other values. They can be members of otherwise meaningful structures, and you can do calculations with these structures. "fst (1, _|_)" is a good and meaningful calculation.

Mere syntax.

So what?

...

Every other Haskell value /does/ have an interpretation.

So, (_|_) is bad, but (1, _|_) is good?

I did not introduce "good" and "bad" into this discussion. I have merely said (in more words) that I want my hypothetical perfect language to prefer OPERATIONAL (model) SEMANTICS for a typed PARACONSISTENT LOGIC over the DENOTATIONAL SEMANTICS which the official documentation sometimes dips into.

Well, that's a different story. But it seems to me that the term "Haskell-like" won't apply to that kind of language. Also, it seems to me (though I don't have any kind of proof) that denotational semantics is something that is much simpler.

It is clear that denotational semantics is a Platonic model of constructive computation.

Could you please stop offending abstract notions?

Then you are mistaken. I am talking about choosing the appropriate mathematical model of computation to accurately, clearly, and simply describe the language's semantics.

Well, domain theory does exactly that for Haskell.

On Thu, Dec 22, 2011 at 4:19 AM, Heinrich Apfelmus wrote:

Alexander Solla wrote:

...

...

And denotational semantics is not just nice. It is useful. It's the best way to understand why the program we just wrote doesn't terminate.

Denotational semantics is unrealistic.  It is a Platonic model of constructive computation.  Alan Turing introduced the notion of an "oracle" to deal with what we are calling bottom.  An oracle is a "thing" that (magically) "knows" what a bottom value denotes, without having to wait for an infinite number of steps.  Does Haskell offer oracles?  If not, we should abandon the use of distinct bottoms.  The /defining/ feature of a bottom is that it doesn't have an interpretation.

Huh? I don't see the problem.

Introducing bottom as a value is a very practical way to assign a well-defined mathematical object to each expression that you can write down in Haskell. See

 http://en.wikibooks.org/wiki/Haskell/Denotational_semantics

It's irrelevant whether _|_ is "unrealistic", it's just a mathematical model anyway, and a very useful one at that. For instance, we can use it to reason about strictness, which gives us information about lazy evaluation and operational semantics.

As another example.... Not that long ago, Bob Harper was complaining on his blog about how you can't use induction to reason about Haskell functions. But, that's incorrect. What you can't use is induction based on a model where all data types are the expected inductively defined sets, and non-termination is modeled as an effect. This isn't surprising, of course, because Haskell's models (i.e. denotational semantics) aren't like that. But, once you know what Haskell's models are---they model types as domains, and data types are inductively defined _domains_, not sets---then you in fact get induction principles based on those models (see for instance, Fibrational Induction Rules for Initial Algebras). You need to prove two or three additional cases, but it works roughly the same as the plain ol' induction you seem to lose for having non-strict evaluation. And then you have one less excuse for not using a language with lazy evaluation. :) -- Dan * http://personal.cis.strath.ac.uk/~patricia/csl2010.pdf

On 22 Dec 2011, at 17:49, Bardur Arantsson wrote:

Alexander Solla wrote:

...

I happen to only write Haskell programs that terminate. It is not that hard. We must merely restrict ourselves to the total fragment of the language, and there are straight-forward methods to do so.

Do (web/XML-RPC/whatever) server type programs terminate?

No, but "total" and "terminating" are not the same. Those *co*programs will, if they're any good, be total by virtue of their productivity rather than their termination. What's slightly controversial is the claim that we "must merely restrict ourselves to the total fragment of the language". It would be more controversial to claim that some new Haskell-like language should restrict us to total programs. 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. This is not the first time the issue has surfaced, nor will it be the last. It's customary at this point to object that one wouldn't want to program with the monadic notation, just for the effect of partiality. I'd counter that I don't want to program with the monadic notation, for any effects: 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. All the best Conor

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

On 23 Dec 2011, at 02:11, Conor McBride wrote:

...

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.

Oh, so it's not an arbitrary monad, but a single one. That's a bit disappointing.

On 2011-12-23 13:46, Conor McBride wrote:

...

...

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.

The list of effects is arbitrary, and localizable, by means of defining handlers. So it's not a single monad.

It's probably still disappointing.

On the contrary!

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.

I was drawn to call-by-push-value a few years ago while attempting to create a language which would support both call-by-value and call-by-name. I haven't had the skill to express what I have felt to be the shortcoming of Haskell, but I believe you've put your finger right on it.

it's an attempt to re-rationalise techniques that emerged from Haskell programming. Exactly.

Haskell has grown a wealth of features/libraries/techniques for combining monads, yet the fundamental monad, evaluation, has a separate place in the language. -- Scott Turner

On Dec 21, 2011, at 2:24 PM, Alexander Solla wrote:

I would rather have an incomplete semantic, and have all the incomplete parts collapsed into something we call "bottom". We can then be smart and stay within a total fragment of the language (where bottom is guaranteed to not occur).

But part of the whole point of including bottom in our semantics in the first place is *exactly* to *enable* us to be smart enough to know when we are staying within a total fragment of the language. For example, including bottom in our semantics allows us to make and prove statements like fst (42,_|_) = 42 and fst _|_ = _|_ That is, as long a you know that the pair is total and that the first element is total, calling fst on it is also total regardless of whether the second value is total. Refusing to use bottom in our semantics doesn't make life better by forcing us to stay within a total fragment of the language, it actually makes life harder by removing from us a useful tool for knowing *how* to stay within a total fragment of the language. Cheers, Greg

I would make the 'type' symbol a single character ala Agda. For example, a : Int If your users are writing a lot of types, make it easy! On Dec 22, 2011 10:42 AM, "Alexander Solla" wrote:

On Tue, Dec 20, 2011 at 10:30 PM, Gregory Crosswhite < gcrosswhite@gmail.com> wrote:

...

On Dec 21, 2011, at 2:24 PM, Alexander Solla wrote:

I would rather have an incomplete semantic, and have all the incomplete parts collapsed into something we call "bottom". We can then be smart and stay within a total fragment of the language (where bottom is guaranteed to not occur).

But part of the whole point of including bottom in our semantics in the first place is *exactly* to *enable* us to be smart enough to know when we are staying within a total fragment of the language. For example, including bottom in our semantics allows us to make and prove statements like

fst (42,_|_) = 42

A proof:

fst :: (a,a) -> a fst (a,b) = a

and

...

fst _|_ = _|_

This expression is basically non-sense. Should we accept straight-forwardly ill-typed expressions like:

data Strict a = Strict !a fst (Strict [1..])

just because the argument is "strictly" a bottom? Bottom inhabits every type, but only vacuously.

To be generous in my interpretation, I assume you mean something like:

fst (_|_, 10) = _|_.

That is still proved by fst (x,y) = x

Things like seq, unsafeCoerce, and the like, are defined as (functions into) bottom in GHC.Prim, and the real semantic-changing magic they perform is done behind the scenes. It cannot be expressed as Haskell in the same Haskell context it is used. So assuming you mean something like:

fst (seq [1..] (1,2))

I must respond that you are using one of these magical keywords which change Haskell's semantics. They should be avoided.

...

Refusing to use bottom in our semantics doesn't make life better by forcing us to stay within a total fragment of the language, it actually makes life harder by removing from us a useful tool for knowing *how* to stay within a total fragment of the language.

I am collapsing the semantics for "distinct" bottoms into a single bottom and noting that it has no interpretation as a Haskell value.

Notice that this brings Haskell's type theory in line with ZF and typed set theories. In those theories, bottom merely exists as a syntactic expression with no interpretation. It is the proto-value which is not equal to itself. We can say that it inhabits every type. But that is only vacuously. Bottom does not exist.

We can stay in the total fragment of Haskell very easily, essentially by using my quotient construction for bottom:

http://www.cse.chalmers.se/~nad/publications/danielsson-et-al-popl2006.html

It requires a shift of point of view, from denotational semantics and "computational effects" (the things we're trying to avoid by going functional and lazy!) to the language of logic, proof, and interpretation. It is possible, consistent, and much simpler conceptually and in use.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Отправлено с iPhone Dec 20, 2011, в 7:10, Alexander Solla написал(а):

* Documentation that discourages thinking about bottom as a 'value'. It's not a value, and that is what defines it.

It's definitely a value.

John Meacham :

The fact that bottom is a value in Haskell is the fundamental thing that differentiates Haskell from other languages and the source of its power. The fact that f _|_ /= _|_ potentially _is_ what it means to be a lazy language. Not treating _|_ as a value would be a huge disservice to anyone learning the language. Sure, it may seem a little strange coming from the imperative world to think of it as a value, but it is by far the oddest concept in Haskell, after all, _functions_ are values in Haskell and people seem to eventually figure that out. Well... Personally I hate thinking about bottom as "value". I don't do this. I NEVER teach that. And, I am a "lazy guy", almost all my Haskell programs are strongly based on laziness.

I'll tell you what I teach, and you might throw some tomatoes... "The fundamental thing that differentiates Haskell from other languages and the source of it power" - if I might cite you - is that we don't see the difference between an object and the process which creates it. (The difference demands that we speak about the call-by-need, etc...) The bottom, as sin (2*pi), or "Text" may be seen as processes. Anyway, a lazy list IS a process /par excellence/. The _|_ entity is a process which refuses to give you a value (or does it in a deadly way). Your program manipulates processes. A process in some computational context must do something - or not. The bottom never does anything useful. All this is probably a question of language, of terminology, of preconceptions (of all that, what for God knows which reasons, Americans call "just semantics"), but I will not forget the day when I thought as you, and I had to explain to 2-nd year students what does it mean: a value which doesn't have a value... Thank you. Jerzy Karczmarczuk

Jerzy Karczmarczuk wrote:

Well... Personally I hate thinking about bottom as "value". I don't do this. I NEVER teach that. And, I am a "lazy guy", almost all my Haskell programs are strongly based on laziness.

I'll tell you what I teach, and you might throw some tomatoes... "The fundamental thing that differentiates Haskell from other languages and the source of it power" - if I might cite you - is that we don't see the difference between an object and the process which creates it. (The difference demands that we speak about the call-by-need, etc...) The bottom, as sin (2*pi), or "Text" may be seen as processes. Anyway, a lazy list IS a process /par excellence/. The _|_ entity is a process which refuses to give you a value (or does it in a deadly way). Your program manipulates processes. A process in some computational context must do something - or not. The bottom never does anything useful.

While it's ultimately an issue of nomenclature, applying the terminus "value" to _|_ is a good idea, because it allows us to answer questions like the following: Question: What is (the denotation of, the value of) x = and $ take 5 $ cycle [True,False] where cycle xs = fix (xs++) Answer: x = False If you treat _|_ as a value, this answer can be obtained by straightforward algebraic manipulation. If you treat _|_ as an operational construct, you will have to perform graph reduction to see the answer, but then you have to worry about the *order* in which you perform your reduction steps. It's not wrong to perform graph reduction, and any student should do it at one point in their lives, but the restriction to operational semantics would miss an important abstraction that is part of the Haskell spirit. Best regards, Heinrich Apfelmus -- http://apfelmus.nfshost.com

On Dec 20, 2011, at 8:05 PM, Tillmann Rendel wrote:

Hi,

Robert Clausecker wrote:

...

Image you would create your own language with a paradigm similar to Haskell or have to chance to change Haskell without the need to keep any compatibility. What stuff would you add to your language, what stuff would you remove and what problems would you solve completely different?

I would try to improve the language's support for the embedding of domain-specific embedded languages (aka. combinator libraries). Such embedding requires the integration of a domain-specific language's syntax, static semantics and dynamic semantics. Some (more or less far fetched) ideas about these three areas follow.

To support better syntax for embedded languages, provide more rebindable syntax à la do-notation. For example, (if c then t else e) currently desugars to (case c of False -> e; True -> t). But it could also desugar to (if' c t e) where if' is a method of a type class. For (c : Bool), the standard library would provide an instance of this type class, but for other condition types, third-party libraries could provide it. Alternatively, if-then-else could even desugar to whatever if' is in scope. A similar idea is currently applied to Scala in the scala-virtualized project. A large part of the language should be virtualized this way, including pattern matching, lambda expressions, maybe even type or class declarations.

To support better static semantics for embedded languages, provide better type-level computation, including some form of closed-world reasoning (for example, backtracking or closed pattern matching) and a reification of names at the type level, so that type-level computations can reason about the binding structures of expressions-level code. Note that I am interested in the static structure of terms, not their dynamic behavior, so this is different from dependent types.

With Haskell being a fine general-purpose programming language, and even having a good foreign language interface, there is already plenty of support for the specification of dynamic semantics. Nevertheless, for domain-specific embedded compilers, it would possibly be nice to access a Haskell compiler at runtime, to compile snippets of Haskell code and dynamically link them into the currently running program.

So in other words, you would like Haskell to simultaneously become more like Lisp and more like Agda? :-) Cheers, Greg

On Dec 20, 2011, at 11:18 PM, Heinrich Apfelmus wrote:

Tillmann Rendel wrote:

...

Hi, Robert Clausecker wrote:

...

Image you would create your own language with a paradigm similar to Haskell or have to chance to change Haskell without the need to keep any compatibility. What stuff would you add to your language, what stuff would you remove and what problems would you solve completely different? I would try to improve the language's support for the embedding of domain-specific embedded languages (aka. combinator libraries). Such embedding requires the integration of a domain-specific language's syntax, static semantics and dynamic semantics. Some (more or less far fetched) ideas about these three areas follow.

I think this is a very good point. The things I would like to see:

* Better syntax for observable sharing. Doaitse Swierstra proposed a "grammer" construct that is basically a let statement where the binder names can be observed. I'm not entirely sure whether that is the most general or sufficient syntax, but something along these lines.

* Meta-programming / partial evaluation. When designing a DSL, it is often the case that you know how to write an optimizing compiler for your DSL because it's usually a first-order language. However, trying to squeeze that into GHC rules is hopeless. Having some way of compiling code at run-time would solve that. Examples: ** Conal Elliott's image description language Pan ** Henning Thielemann's synthesizer-llvm

I am not disagreeing with anything that you have said here, but in a way it seems like the problem is more fundamental than all of these things since metaprogramming and type-programming in Haskell is not first-class, so it really isn't a language that is designed for DSLs even though people get a surprisingly long way abusing it for this purpose. :-) Really what we need is a language built from the ground up for this purpose, such as Lisp, but without the parts of Lisp that cause us to use Haskell instead. :-) Cheers, Greg

One thing that concerns me is the use of capital letters to distinguish type and class names and constructors from values.  If I was doing it over I would use a typographical distinction like italics for types, bold for classes.  That way we could have a constructor named ∅, a function named ∈, a class named ℝ.

It's Algol all over again! Will we have to typeset our keywords in bold too?

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Tue, Dec 20, 2011 at 11:17:32PM +0100, Hans Aberg wrote:

The monospace characters U+1D670-1D6A3 might be used for keywords. Font: http://www.stixfonts.org/

I feel that monospace fonts should be used for all of programming. A language could use Unicode symbols, but if it enforces typography, it is destined to win an award for being really unusable

IIRC, Scite's default configuration is with non-monospace font. I actually found it quite appealing, and in fact forgot about it entirely after some usage. It is much easier on the eyes to read. The difference is really whether you care about aligning things mid-line or not, not to mention editor support (i.e. not Vim or other terminal-based editor). On Wed, Dec 21, 2011 at 8:58 PM, Hans Aberg wrote:

On 21 Dec 2011, at 04:27, Ashok Gautham wrote:

...

On Tue, Dec 20, 2011 at 11:17:32PM +0100, Hans Aberg wrote:

...

The monospace characters U+1D670-1D6A3 might be used for keywords. Font: http://www.stixfonts.org/

I feel that monospace fonts should be used for all of programming. A language could use Unicode symbols, but if it enforces typography, it is destined to win an award for being really unusable

I have some books from the 1980s which does not use monospace; it seems to be a later movement. Using it for all symbols would be awkward.

Hans

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On 21 Dec 2011, at 11:22, Andrew Coppin wrote:

On 21/12/2011 10:09 AM, Jesse Schalken wrote:

...

IIRC, Scite's default configuration is with non-monospace font. I actually found it quite appealing, and in fact forgot about it entirely after some usage. It is much easier on the eyes to read. The difference is really whether you care about aligning things mid-line or not, not to mention editor support (i.e. not Vim or other terminal-based editor).

SciTE's default binding /is/ proportional, not mono-space. I find it ever so irritating. Then again, I'm sure this one comes squarely down to personal preference, so it seems pointless to debate it.

LaTeX offers the possibility of mid-line alignment even if you don't use monospace - a feature which I haven't seen in any other text processing system. It's a pitty this isn't more widespread...

Monospace isn't used in math (except in the days when one used typewriters), but alignments are of course used in matrices and multiline formulas, for example, which may correspond to uses in computer code. A problem is that LaTeX is used for rendering typeset pages, and not really suitable for writing direct computer code, though Unicode characters can improve the readability of LaTeX source code. The link below shows an example. Hans http://www.charlietanksley.net/philtex/the-unicode-math-package-for-xelatex-...

With GHC 7.0.3: $ cat test.hs class ℝ a where { test :: a; }; (∈) :: Eq a => a -> [a] -> Bool; x ∈ (y:ys) = x == y || x ∈ ys; main = putStrLn "Two of three ain't bad (^_~)"; $ runhaskell test.hs Two of three ain't bad (^_~) $ On 20/12/2011, David Fox wrote:

On Mon, Dec 19, 2011 at 11:20 AM, Robert Clausecker wrote:

...

Image you would create your own language with a paradigm similar to Haskell or have to chance to change Haskell without the need to keep any compatibility. What stuff would you add to your language, what stuff would you remove and what problems would you solve completely different?

Thanks in advance for all answers, yours

One thing that concerns me is the use of capital letters to distinguish type and class names and constructors from values. If I was doing it over I would use a typographical distinction like italics for types, bold for classes. That way we could have a constructor named ∅, a function named ∈, a class named ℝ.

Cheers, Matthew Farkas-Dyck

On Tue, Dec 20, 2011 at 3:10 PM, Chris Wong wrote:

Why not expand it even further?

class Monoid m where    (•) :: m -> m -> m    (∅) :: m

(∈) :: (Foldable t, Eq a) => a -> t a -> Bool

(∘) :: (b -> c) -> (a -> b) -> (a -> c)

(∧) :: Bool -> Bool -> Bool

etc.

We can write a whole Haskell library full of these aliases -- "syntactic-heroin" perhaps? ;)

Why would you go that far and still not have → ? (: martin

On Tue, 2011-12-20 at 16:53 -0500, Matthew Farkas-Dyck wrote:

Two of three ain't bad (^_~)

Now we just need λ to replace \, → to replace ->, and ≠ to replace /= (which still looks like division assignment no matter how hard I squint my eyes. 25 years of C and C derived languages is hard to forget). Hey, forget replacing, wouldn't it be wonderful if the compiler would just accept them as synonyms? AfC Sydney

On 21 Dec 2011, at 04:15, Brandon Allbery wrote:

On Tue, Dec 20, 2011 at 21:05, Andrew Cowie wrote:

...

Now we just need λ to replace \, → to replace ->, and ≠ to replace /= (which still looks like division assignment no matter how hard I squint my eyes. 25 years of C and C derived languages is hard to forget). Some of it is already supported. http://www.haskell.org/ghc/docs/latest/html/users_guide/syntax-extns.html#un...

(≠ isn't in that list, but it doesn't need to be; just stick it in the Prelude if it's not there already, since it's not special syntax, it's just another operator. The * *is* a special case, I suspect, though: I bet it's only supported in kinds, not as the multiplication operator.)

The one on the list is not a mathematical symbol. It should be ⋆ STAR OPERATOR U+22C6 or ∗ ASTERISK OPERATOR U+2217.

The problem with λ is that it's a perfectly valid Unicode lowercase letter. There is 𝛌 MATHEMATICAL BOLD SMALL LAMDA U+1D6CC but font support is often lacking, and it looks like Unicode categorizes *that* also as a lowercase letter. If you can convince the Unicode Consortium to add a lambda that is of class symbol, Haskell can then make use of it — once there are fonts that support it.

There is http://www.stixfonts.org/ For typesetting with Xe[La]TeX or Lua[La]TeX, use XITS (in the TeXLive package).

(And then we'll have to deal with folks trying to use the letter, because everyone knows the Roman alphabet is the only one that matters and of *course* Greek letters are symbol characters.... Pfeh.)

This is the big problem right now: how to enter these symbols efficiently. Hans

On 21 Dec 2011, at 11:03, Brandon Allbery wrote:

On Wed, Dec 21, 2011 at 04:51, Hans Aberg wrote:

...

The one on the list is not a mathematical symbol. It should be ⋆ STAR OPERATOR U+22C6 or ∗ ASTERISK OPERATOR U+2217.

...except, at least in my current font, the former is microscopic and the latter not a whole lot better. The advantage of the one they chose is it's big and readable. (That's part of why I assume it's intended for kinds, actually.)

This problem is in my editor for unstyled text due to that if it a symbol is not available in the font selected, it just chooses a glyph from the next font available in alphabetical order. Hopefully such problem will be resolved in the future. Hans

I'd suggest, in addition to the symbols, renaming some of the fundamental types and concepts, like Monad. I would violently agree that Monad is the correct term, but try to communicate with a commodity software developer sometime (or a government acquisition professional). RWH goes a long way to explaining the concepts, as do the countless Web pages dedicated to explaining the monad concept. Better examples for SYB and arrows would also help. Haskell is a great language with solid mathematical underpinnings. I'm a big fan of it. But, adoption is the key to success; need to make the ordinary easy to understand unless the community wants to be relegated to Scala status. -----Original message----- From: Andrew Cowie To: haskell-cafe@haskell.org Sent: Tue, Dec 20, 2011 18:05:18 PST Subject: Re: [Haskell-cafe] If you'd design a Haskell-like language, what would you do different? On Tue, 2011-12-20 at 16:53 -0500, Matthew Farkas-Dyck wrote:

Two of three ain't bad (^_~)

Now we just need λ to replace \, → to replace ->, and ≠ to replace /= (which still looks like division assignment no matter how hard I squint my eyes. 25 years of C and C derived languages is hard to forget). Hey, forget replacing, wouldn't it be wonderful if the compiler would just accept them as synonyms? AfC Sydney _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

...

- Function overloading without classes. If it's not done, there must be a good reason for it (many good reasons, probably), but I really miss it.

That does not play well with type inference.

I understand that. But it may be ok in many simple situations, which is actually where I tend to "need" it. For instance, the following wouldn't pose a problem, would it? f :: Int -> Int -> Int f = (+) f :: String -> String -> String f = (++) (Not that I would use it for exactly that code, but anyway). I know that one can write that with classes and instances, but I just want to save myself the extra-coding when possible. In complex situations (where it doesn't play well with type inference), that's when I'd rather create classes and instances. Not for the type-checker, but for myself.

Also, see type-directed name resolution (TDNR) Thanks for that pointer. I found that proposal a few months ago, but had completely forgotten about it.

I don't really like the proposed syntax; it's very OO-like. I agree with gabrielrf, who said "[...] I wonder if adding an obj.method style will be a hinderance to beginners, as it obscures what type inference can do."

In Haskell, most of these assumptions are invalid:

     * something may be curried or member of a strange typeclass (like        printf). No assumptions about the number of arguments can be        made      * It may be possible that we do not yet know the type of a because        we can't infer it's type without knowing the type of x      * show obj is definitely a String      * 2 is of type Num a => a. What if there are two something, one        with a parameter of type Int and one with a Float?

You see, It's not so easy. I see. Thanks for such a clear explanation.

2011/12/22 Gábor Lehel

On Mon, Dec 19, 2011 at 8:20 PM, Robert Clausecker wrote:

...

Image you would create your own language with a paradigm similar to Haskell or have to chance to change Haskell without the need to keep any compatibility. What stuff would you add to your language, what stuff would you remove and what problems would you solve completely different?

Thanks in advance for all answers, yours

Robert Clausecker

I would have compose (probably not called '.') read the same way we read this sentence (and unix pipes) ie left to right. I would not overload . to mean compose and module-access. Probably gadt could be the norm and classic 'data' could be removed.