2008/9/30 Jason Dagit :

...

It seems to me that dependent types are best for ensuring totality.

Bear with me, as I know virtual nothing about dependent types yet. In the total functional paradigm the language lacks a value for bottom. This means general recursion is out and in the paper I cited it was replaced with structural recursion on the inputs. How do dependent types remove bottom from the language?

Most DT languages are total. You have to be able to evaluate terms to typecheck, so in order to have a terminating compiler, your language needs to be bottomless. The other side of that is that dependent types are strong enough to express termination proofs of some very tricky functions, which I suspect would not be possible to prove otherwise. Luke

Jason Dagit wrote:

I was asserting that Haskell is currently 2 layered. Purely functional vs. IO. They integrate nicely and play well together, but I still think of them as distinct layers. Perhaps this is not fair or confusing though. The paper I cited did indeed use codata to define streams so that something, such as an OS, that needs to process infinite streams of requests can still do so.

For a first take on monads, that's not a bad way of thinking about it. But, once you move beyond first thoughts, monads aren't a special separate layer and thinking of them as such is liable to land you in trouble. Monads really are pure, it's just that they get there by existentializing over impurities.[1] Perhaps you really do mean only the IO monad and not any others, but then the question becomes: whose IO? The IO monad is well-known to be a sin bin for things people don't know or care enough about. Over time things get added to IO and over time things get broken off into their own monads. So then where is the layer boundary over time? I assert that there's no meaningful place to draw the boundary because there's nothing particularly special about IO that isn't shared by other monads like ST or ACIO. It'd be nice to have a total core language, but it's not clear how to helpfully represent such things in the type system. One variety of non-totality is the |error| function. We could design our types to say that people can't call it, but the whole purpose of |error| is to raise exceptions (a monadic action) from pure code; so as far as the types are concerned, we already can't do any such things. We can eliminate many instances of those non-totalities by adding in refinement types (a modest proposal), in order to prevent people from passing [] to |head| or |tail|, or passing 0 as the denominator of (/), etc. But there are other non-totalities, such as _|_ which cannot be captured by such means. In order to capture many instances of _|_ we'd need to have our type represent their depth so that we can do co/induction in order to ensure that the function terminates. While we can capture a surprising level of such detail in Haskell's type system, this is marching off in the direction of dependent types which would be making things more complex rather than simpler. I'm not saying that we shouldn't head there, but it doesn't seem to be addressing the goals you had in mind. [1] Just like existential types, you can put something in but you can never get it back out again. For inescapable monads like IO and ST, this is why they have the behavior of sucking your whole program into the existential black-hole. -- Live well, ~wren

David Menendez wrote:

On Wed, Oct 1, 2008 at 7:53 PM, wren ng thornton wrote:

...

[1] Just like existential types, you can put something in but you can never get it back out again. For inescapable monads like IO and ST, this is why they have the behavior of sucking your whole program into the existential black-hole.

That's true for IO, but the whole point of ST is that it *is* escapable. What makes ST (and IO and STM) unusual is that it can't be implemented in pure Haskell without special support from the run-time system.

I suppose it depends on definitions. Certainly you can runST it to get an end result out, but doing so looses the internal structure (STRefs) which cannot be reclaimed. To me this makes ST a world apart from State, [], Maybe, and other monads which you can freely escape and reenter. Perhaps it would've been better to say that ST is not, er, reentrant. -- Live well, ~wren

Hi

for little more than personal taste). In particular, I'd like to see a reasoning framework for partial functions, so you could state and prove a property like:

length [1..] = _|_

In a compiler, with: default(Int) main = print $ length [1..] Results in 2147483647 I don't think dependent types are the answer - or at least I don't think people have asked the questions in standard Haskell enough. We still don't even have an equational reasoning assistant publically available and widely used. Thanks Neil ============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ==============================================================================

On Tue, Sep 30, 2008 at 4:37 AM, Robin Green wrote:

On Tue, 30 Sep 2008 03:27:09 -0600 "Luke Palmer" wrote:

...

But I *want* to do something like that with Coq (I prefer it to Agda for little more than personal taste). In particular, I'd like to see a reasoning framework for partial functions, so you could state and prove a property like:

length [1..] = _|_

Bear in mind, in Coq, the equivalent of [1..] is a stream, whereas the equivalent of [1,2,3] is a list.

You miss my point. Every value here is lifted to its domain before being reasoned about. So eg. [1,1..] is not the coinductive x = 1:x. Instead we model this example like so (this is my current direction, nothing tested or fully reasoned out, so I may be full of beans): [1..] is the limit [_|_, 1:_|_, 1:2:_|_, ...] length [1..] is the limit [_|_, _|_, _|_, ...] Every function we can write in Haskell is corecursive on this representation, because every such function is Scott-continuous. To prove the above property would amount to proving that every element of the resulting limit is _|_, so the whole limit is _|_. Luke

Hi I've been reticent to join this thread as it has the potential to eat my life, but I thought I'd say some technical things. On 30 Sep 2008, at 22:54, Derek Elkins wrote:

On Mon, 2008-09-29 at 20:02 -0700, Jason Dagit wrote:

...

Maybe instead of using (->) as the function constructor for total functions we use a different symbol, say (|->), and the compiler knows to use the more specialized semantics on those definitions. I'm not sure how make this work for values that are total functional versus values that are just pure (partial) functional.

This can be done exactly the same way it is done with IO. Remove general recursion* from Haskell and have a partiality monad with fix :: (a -> a) -> Partial a

I'm not sure that's the best type for fix, to be honest (though it would do in a pinch). It doesn't nest very neatly. Some argue for sfix :: (a -> Partial a) -> Partial a which allows you to make partial computations from recursive values. Being a happy Haskeller, I'd prefer lfix :: (Partial a -> Partial a) -> Partial a which is probably just join . fix as you present it, but says that its body gets a computation which it can choose to run, or not, as appropriate. In the dependently typed world, remember there are two separate notions of operational semantics (1) the open evaluation used by the typechecker, reducing under lambda, etc (2) the closed evaluation used at run-time, with no computation under binders It should be straightforward to make lfix a constant in (1), whilst (2) would actually run it. So that is indeed very like IO, handing off computations to an unscrupulous run-time system. Of course, we'd provide laws to reason about Partial computations (monad laws, unrolling, fixpoint induction) with sufficient means to allow escape from Partial on presentation of a (non-Partial) termination proof (erased for (2)). That's all to say that we can set things up so you can pay as you go. Of course, that's just to say we can model the phenomena, not that we can present them ergonomically... But what of Haskell?

This particular idea has been discussed several times in a couple of places. Most people seem to think it would be too much of a hassle to use.

Not the most copper-bottomed of arguments, as well you know, but if programming in Partial entails clunky monadification of lovely terse applicative code, most people are probably right. However, what if we were to find a way to break that entailment? The idiom bracket notation is a step in that direction, but it's still not enough. Suppose we were to find a way to program with our usual notation, but with the extra freedom to vary the 'ambient' monad? We could choose Id for total programs, Partial for workaday slackness, and a whole bunch of other stuff at our convenience. We'd need some way to change the ambient monad locally, of course. To be frank, I don't know if such a setup could be made to fit with Haskell's existing design choices. But I think it's an attractive possibility, worth looking into. Locally, however, my point is to ask whether there's a specific hassle with the Partial monad beyond the usual notational annoyances that come with any monad. If so, that would be interesting to hear about, and new to my ears. All the best Conor