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

5
votes

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.

3
haskelllazy-evaluationstrictness
Have you seen the Disciple language? – C. A. McCann
Thanks. I was looking for a way to squeeze this into current Haskell (well, GHC that is) but that's interesting as well. – Clinton
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! – Ben
@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. – Andreas Rossberg
@Clinton 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. – Ben

3 Answers

6
votes

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.

1
votes

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.

1
votes

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

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.