Type enforced "strict/imperitive" subset/version of Haskell

Question

I quite like Haskell, however one of the main things that concerns me about Haskell the difficulty in reasoning about space usage. Basically the possibility of thunks and recursion seem to make some tricky situations where it seems one has to be very careful by adding the correct strictness lest the program run out of memory on particular inputs.

What I like about C/C++ is that I can quickly be fairly certain about the upper bounds of a programs space usage, in particular if one avoids recursion. The variables are clear to see.

What I was wondering is if there's a way to create a typesafe "imperative" subset of Haskell, which doesn't have thunks, and is strict.

I understand Data.STRef gives mutable cells, but as far as I understand these cells themselves are still lazy and can contain thunks. I was thinking to force the data in such cells to be strict, but I'm unsure how to do this in a manner enforced by the type system.

I was thinking something like a "Strict Monad" but perhaps that isn't the correct form to do this in.

Turboprop

Have you seen the Disciple language? – Alaska

Thanks. I was looking for a way to squeeze this into current Haskell (well, GHC that is) but that's interesting as well. – Turboprop

The prevalence of memory leaks in programs with manual memory management kind of disproves your thesis that it's easy to establish upper bounds of a C/C++ programs's space usage. That said, excellent question! – Bio

Ben: Memory leaks are pretty easy to avoid in C++ by just using RAII and smart pointers (if necessary). It's only with cyclic data structures that things get tricky, but most data structures I've worked with aren't cyclic. – Turboprop

If you want a strict and/or impure functional language, why not use one? There is OCaml, for example. – Bashemath

@Clinton, oh, and as A C++ developer, I deeply disagree with memory management being "pretty easy". It's difficult in general, and moreover, there are many abstractions you simply cannot do because of it. – Bashemath

What can't you do without smart pointers and RAII? Besides circular stuff? – Turboprop

@Turboprop That's a bit like saying "Space leaks are pretty easy to avoid in Haskell by just pipe-lining your data and using stricness annotations (if necessary)". Of course there are ways to avoid space problems by programming carefully, but it's guaranteed to go wrong occasionally because all code has bugs. – Bio

@Ben: As far as I know, in C++, you just use new in the constructor and delete in the destructor, and otherwise use smart pointers. There's no "(if necessary)", and I'm not sure what "pipe-lining" means? – Turboprop

@Clinton, for starters, this is not a smart pointer, and cannot be wrapped. Anything to do with non-trivial closures becomes a major nightmare as well. Or concurrency. And many abstractions become extremely leaky with manual memory management, to the point of rendering them useless. – Bashemath

Answer 1

I'm fairly sure it would be next to impossible to implement this in Haskell, which really assumes laziness by default. For example, there are functions all through the standard library which would be useless in a strict language because they are in fact guaranteed not to terminate if you request their entire output. So if you had a "strict subset" of Haskell, it would be difficult to interoperate with any other Haskell code, and you'd effectively be programming in another language anyway.

Also, I think you're looking in the wrong place by thinking about monads. Data.STRef indeed has nothing to do with avoiding thunks and laziness. In fact what you want (strictness) has nothing to do with being imperative, and you don't need mutability or monads to get it. There are programming languages which are just as pure as Haskell, but strict everywhere. One I have worked with is Mercury, for example.

Bio

I thought that Mercury is not strict. The reason why it strict that it should check each prerequisite for goal (composed by conjunction , ) while with disjunction (;) it can choose. And as I know it can re-order anything while keeping di/uo (destroyed input/ unique output used for representing IO-like things). P.S. That's good to know that there is another person who saw Mercury and spreads the fact of existing such languge. – Oneway

@Oneway Disjunctions are non-strict only in the same way that if/then/else is non-strict in every language; you can't really have branching if all branches are fully evaluated before one is picked! The language is generally strict, in that calling predicate(Input, Output) will return with Output bound to a fully evaluated value (no thunks), and if Output is infinite then the call will not terminate even if you don't need to use Output for anything. – Bio

@Oneway It is a little more complicated due to backtracking/nondeterminism, though, so in that sense you're right. predicate might be able to be resumed to produce another Output if something fails at a higher level, so the data it had a reference to might be kept in memory in case that happens. It's not really the same thing as runaway thunk-generation due to non-strictness in Haskell, and generally much more intuitively predictable from the determinism class of the predicates. – Bio

Answer 2

You might be interested in reading about BangPatterns language extension and Unboxed types/operations. But you also should know the fact any function will always have meaning of boxed type. That's responsibility of optimization to eliminate any ref-kind values by compiling code according to "bangs" and other stuff into functions.

Oneway

Answer 3

I've thought about this a bunch. So have other people:

• Mailing list thread
• GHC ticket
• Another mailing list thread

Now my own speculation.

In the above discussions, the basic idea most of the time is that you could stick a ! on any type to get a strict, definitely evaluated, WHNF version of that type. So Int might be a thunk, while !Int is definitely not one. That raises interesting questions for the typechecker. Does !Int ~ Int hold? If it doesn't -- the two are completely separate, incompatible types -- then working with them would be very painful. On the other hand, if it does hold, there would be nothing to prevent passing an unevaluated Int where an !Int is expected -- after all, they are the same type. What you would ideally want is to be able to supply an !Int where an Int is expected, but not vice versa. That sounds like a subtype relationship: !a <: a, !a is a subtype of a, a is inhabited by both evaluated and unevaluated values (thunks), while !a only by evaluated ones. GHC's type system doesn't have subtyping, and probably couldn't, because the other parts of the type system don't interact well with it. This is a highly restricted, specific instance of subtyping though: the programmer doesn't get to declare arbitrary subtype relationships, rather there exists a single, hardcoded relationship: forall a. !a <: a. I have no clue whether or not that makes it more reasonable to implement.

Suppose it could be done. You get further questions. What if you do try to supply an Int where an !Int is expected? Type error? Ideally, I think, it wouldn't be, instead the compiler would insert code to evaluate it, and carry on. Okay. How about supplying [Int] where [!Int] is expected, or f a and f !a in the general case? How could the compiler possibly know how to traverse any given structure to find those points where it contains an a, to evaluate those, and only those? So would that be a type error? Let's say it is. How does the programmer do the conversion manually -- get an f !a from an f a? Perhaps by mapping a function eval :: a -> !a? But that's nonsensical. Haskell is pervasively lazy. If you apply it to an argument, eval x, then until its value is needed, it will be a thunk. So eval x can't possibly have type !a. Strictness annotations in the return type position don't make any sense. So what about: data Wrap a = Wrap { unwrap :: a }, eval' :: a -> Wrap !a, with the semantics that Wrap !a might be a thunk, but the compiler inserts code so that when you evaluate it, the !a inside will definitely be evaluated as well? Actually, here's a simpler formulation: data Wrap' a = Wrap' { unwrap' :: !a } (eval' = Wrap'). Which is existing legal Haskell, subsumed by our new strictness typing. That's nice, I guess. But as soon as you try to use it, you get problems again. How would you get from f a to f !a, again -- fmap unwrap . fmap Wrap? But unwrap has the exact same problem as eval. So all of this seems not so trivial. And what about the seemingly innocuous reverse case: supplying f !a where f a is expected? Does that work? (In other words, f !a <: f a?) It depends on how a is used inside of f. The compiler would have to have knowledge of covariant, contravariant, and invariant type argument positions -- another thing that comes with subtyping.

This is as far as I've thought it through. It seems harder than it seems.

One more interesting thing. You may or may not have heard about the notion of unlifted types: types which aren't inhabited by bottoms. That's, as far as I can tell, the same thing as this is. Types which are guaranteed to be evaluated to WHNF; types which are guaranteed to not be bottom. No difference, right? GHC actually already has a bunch of unlifted types as primitives (Int#, etc.), but they're wired in (you can't add new ones) and also unboxed in addition to being unlifted, so they have a different kind (# instead of *) and can't mix with normal types. Whereas !a would be an unlifted, but boxed, type, of kind *. Unlifted types are something I've seen mentioned a few times in type theoretic contexts, so maybe there's been some research into what it would take to implement them in a more general way. I haven't looked, yet.

Countermove