«
»

Lazier functional programming, part 1

11th September 2010, 04:57 pm

This post is inspired by a delightful insight from Luke Palmer. I’ll begin with some motivation, and then propose a puzzle.

Consider the following definition of our familiar conditional:

ifThenElse :: Bool → a → a → a
ifThenElse True  t f = t
ifThenElse False t f = f

In a strict language, where there are only two boolean values, these two clauses have a straightforward reading. (The reading is less straightforward when patterns overlap, as mentioned in Lazier function definitions by merging partial values.) In a non-strict language like Haskell, there are three distinct boolean values, not two. Besides True and False, Bool also has a value ⊥, pronounced “bottom” for being at the bottom of the information ordering. For an illustration and explanation of information ordering, see Merging partial values.

Note: In Haskell code, ⊥ is sometimes denoted by “undefined“, which can be confusing, because the meaning is defined precisely. There are many other ways to denote ⊥ in Haskell, and it is impossible to determine whether or not an arbitrary Haskell expression denotes ⊥. I’ll generally use “⊥” in place of “undefined” in this post, as well as for the corresponding semantic value.

The two-clause definition above only addresses two of the three possible boolean values explicitly. What, if anything, does it say indirectly about the meaning of an application like “ifThenElse ⊥ 3 5“?

The Haskell language standard gives an operational answer to this question. Clauses are examined, using pattern matching to select a clause and instantiate that clause’s variables. In case more than one clause matches, the earlier one is chosen.

Pattern matching has three possible outcomes:

  • A single substitution, providing variable bindings that specialize the patterns in a clause’s left-hand side (LHS) to coincide with the actual call. The matching uses semantic, not syntactic, equality and can require forcing evaluation of previously unevaluated thunks (delayed computations).
  • Proof of the nonexistence of such a substitution.
  • Neither conclusion, due to an error or nontermination during evaluation.

In this example, the effort to match True against ⊥ leads to the third outcome. For Haskell as currently defined, the result of the application in such a case is then defined to be ⊥ also. Which is to say that ifThenElse is strict (in its first argument).

So strictness is the Haskell answer, but is it really the answer we want? Are there alternatives that might better fit the spirit of non-strict functional programming?

Note: Haskell is often referred to as a “lazy language”, while a more precise description is that Haskell has non-strict semantics, typically with a lazy implementation. I think of programming languages and libraries (at least ones I like using) as having a single semantics, amenable to various implementations. (Haskell falls somewhat short, as explained in Notions of purity in Haskell.) Sadly, I don’t know a pleasant comparative form to mean “less strict”, so I’m using the more familiar term “lazier” in this post’s title. Suggestions welcome.

Sums

Now consider a broader example, taken from the standard Haskell prelude, namely sum types and corresponding case analysis:

data Either a b = Left a | Right b

either :: (a → c) → (b → c) → Either a b → c
either f g (Left  x) = f x
either f g (Right y) = g y

Again, these two clauses have a clear and direct reading for strict languages, but in a non-strict language like Haskell, there is a third element of Either a b not explicitly addressed, namely ⊥. Again, Haskell’s current definition says that either f g ⊥ == ⊥, i.e., either f g is always strict.

Products

Most types can be built up from sums and products. Since we’ve looked at sums already, let’s now consider products. And rather than n-ary products, just look at binary products and the unit type (a sort of nullary product).

fu :: () → Int
fu () = 2

fp :: (a,b) → Int
fp (x,y) = 3

Again, these clauses only capture the non-⊥ part of their domains explicitly. And again, the Haskell specification says that these functions are strict.

Here’s a less trivial example:

q :: Bool → (Int,Int) → Int
q b (x,y) = if b then 3 else x

Haskell semantics says that q True is strict, rather than being equivalent to the non-strict function const 3.

Lazier functional programming

Given that we’re enjoying some of the benefits of a non-strict language and programming paradigm (as described, e.g., in Why Functional Programming Matters), we might enjoy more if we can loosen up some of the strictness of pattern-based definitions.

What might a less-strict interpretation be? Let’s take the definition of either above.

I’d require any interpretation to satisfy a two conditions:

  • The meaning is consistent with the direct explicit readings of the clauses. When read as equations, those clauses are true of the meaning of either.
  • The meaning of either f g must be information-monotonic, i.e., more information in leads to more (and consistent) information out.

For an interpretation that is ideal for non-strict programming, I’ll add a third condition:

  • Information-wise, the interpretation is maximal among all meanings that satisfy the first two conditions, i.e., it’s minimally strict.

A puzzle

I’ll end this post with a puzzle: what is a minimally strict interpretation of the definition of either above? Backing up,

  • Is there a meaning for either that satisfies these three conditions?
  • If so, is there exactly one such meaning?
  • If so, what is that meaning, and how can it be obtained and implemented systematically?

Edit: *Warning: spoilers ahead in the comments. I encourage you to play with the puzzle on your own before reading on.

Tags: ,  |  Comment (RSS)  |  Trackback

21 Comments

  1. augustss:

    You don’t say what we have at our disposal to solve the puzzle. If we are restricted to lambda definable functions there isn’t much to do. If we have something like por it’s a different matter.

    11 September 2010, 9:59 pm

  2. Greg:

    After reading “The Implementation of Functional Programming Languages” I had assumed that Haskell (specifically GHC) would use lazy product-matching semantics, as described here:

    http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/PAGES/072.HTM

    Testing with ghci quickly shows that this is not the case, as you’ve said. How disappointing.

    12 September 2010, 9:15 am

  3. Janis Voigtländer:

    Possibly related and of interest: http://korsika.informatik.uni-kiel.de/~jac/wordpress/projects/sloth/

    12 September 2010, 10:11 am

  4. Albert Lai:

    Although some CPOs do not support 2-argument meet (infimum, greatest lower bound) (there is a 5-point example), it seems CPOs for common data types do: flat CPOs for primitive types, product, sum, function space, probably even recursive data types over those. With meet, we can do minimally strict conditional branching.

    (Notation: I use “bool” for “ifThenElse”.) (Notation: “=” means math equal, not program code.)

    We first require:bool True x y = x, bool False x y = y

    Add monotonicity, this implies: bool ⊥ x y ⊑ x, bool ⊥ x y ⊑ y

    If we have meet, it satisfies the above plus minimal strictness: bool ⊥ x y = x⊓y

    Here are some concrete examples. If x,y are distinct numbers (flat CPO), unsurprisingly and can’t be helped, bool ⊥ 3 4 = ⊥

    But then we can have bool ⊥ 3 3 = 3

    More interestingly, x,y are from a richer data type and have something in common: bool ⊥ (0:0:⊥) (0:⊥) = 0:⊥

    The story for either is similar: either f g ⊥ = f⊥ ⊓ g⊥

    For example, perhaps f⊥=0:0:⊥, g⊥=0:⊥, so either f g ⊥ = 0:⊥

    This scheme is also pretty computable — certainly doable for flat types, products, sums, many recursive data types. (I’m too lazy to do functions, but perhaps that’s exactly the right way: lazily.) To evalute bool b x y, speculately evaluate all of b, x, y. As long as x and y churn out common stuff, that goes into part of the answer; at the first point they differ, now wait for b to finish before you commit to the correct branch. To evaluate either f g e, speculatively evaluate all of f⊥, g⊥, e. As long as f⊥ and g⊥ churn out common stuff and haven’t needed what’s inside e yet, that goes into part of the answer; at the first point they differ or one of them needs what’s inside e, now wait for e to finish before you go on.

    Speculative evaluation is natively supported in the futuristic (but commercially unsuccessful) IA64 family. Alternatively it can be done by concurrency and a few sync points. I guess por works too.

    12 September 2010, 5:35 pm

  5. kmc:

    Greg:

    You can obtain the lazy behavior in Haskell with an irrefutable pattern match. In SPJ’s example:

    combine x ~(od,ev) = ...

    This works for sums as well as products, but will result in a runtime exception if the wrong constructor is chosen.

    12 September 2010, 6:16 pm

  6. dimitar:

    My guess after skimming through the linked posts:

    lazierEither :: (HasLub c) => (a -> c) -> (b -> c) -> Either a b -> c
lazierEither f g = (f . fromLeft) `lub` (g . fromRight)

    13 September 2010, 3:58 am

  7. Justin:

    What if either returns a tuple?

    either :: (a -> c) -> (b -> d) -> Either a b -> (c, d)
either f g v = 
  let ~(Left a) = v
      ~(Right b) =  v
  in (f a, g b)
    13 September 2010, 11:24 am

  8. David Sankel:

    Am I getting close?

    either :: Eq c ⇒ (a → c) → (b → c) → Either a b → c
either f g e = t1 `unamb` t2
  where t1 = let a = f undefined
                 b = g undefined
             in if a == b then a else undefined
        t2 = case e of Left a → f a
                       Right b → g b

    13 September 2010, 1:48 pm

  9. David Sankel:

    Oops, want to make that a bit more lazier.

    either :: Eq c ⇒ (a → c) → (b → c) → Either a b → c
either f g e = t1 `unamb` (t2 `unamb` t3)
  where t1 = let a = f undefined
                 b = g undefined
             in if a == b then a else undefined
        t2 = let a = f undefined
                 b = g undefined
             in if a == b then b else undefined
        t3 = case e of Left a → f a
                       Right b → g b

    13 September 2010, 2:02 pm

  10. conal:

    Thanks for the suggested solutions so far. There’s room for correction and/or refinement in all of them, so please pitch in and make suggest improvements.

    13 September 2010, 2:31 pm

  11. Greg M:

    @Vanis: Related to the concurrency issue, Lyndon While published a few papers in the early 2000s on parallel pattern-matching (yeah misnomer, it’s concurrent), aiming for least-strict semantics for pattern-matching. I helped him implement a PPM-Haskell -> Standard-Haskell source transformation.

    13 September 2010, 6:10 pm

  12. David Sankel:

    lazierEither does not meet the consistancy requirements for lub. consider:

    lazierEither (const True) (const False)

    ⇓

    (const True . fromLeft) `lub` (const False . fromRight)

    13 September 2010, 6:55 pm

  13. David Sankel:

    Making my version more efficient.

    either :: (Eq c, Lub c) ⇒ (a → c) → (b → c) → Either a b → c
either f g e = t1 `unamb` t2
  where t1 = let a = f undefined
                 b = g undefined
             in if a == b then (a `lub` b) else undefined
        t2 = case e of Left a → f a
                       Right b → g b

    13 September 2010, 7:02 pm

  14. David Sankel:

    using lub instead of unamb would make my version a bit lazier.

    14 September 2010, 5:34 am

  15. dimitar:

    Yeah, my guess is broken. I was naive hoping that the restriction f ⊥ ≡ g ⊥ can be relaxed.

    14 September 2010, 10:42 am

  16. Dave:

    The opposite of ‘strict’ is ‘lax’, so ‘less strict’ would be ‘laxer’.

    15 September 2010, 5:29 am

  17. dimitar:

    I was wrong again: f ⊥ ≡ g ⊥ is too strong. From Albert Lai’s explanation the minimal strictness is achieved when: either f g ⊥ = f⊥ ⊓ g⊥. In Haskell:

    either :: (HasLub c, HasGlb c) => (a -> c) -> (b -> c) -> Either a b -> c
either f g x = (f undefined) `glb` (g undefined) `lub` strictEither f g x

    When c is flat domain it is essentially David Sankel’s solution.

    15 September 2010, 7:00 am

  18. David Sankel:

    @dimtar: Awesome!

    16 September 2010, 6:34 am

  19. conal:

    You don’t say what we have at our disposal to solve the puzzle. If we are restricted to lambda definable functions there isn’t much to do. If we have something like por it’s a different matter.

    augustss: I didn’t want to bias people’s explorations.

    18 September 2010, 12:55 pm

  20. Conal Elliott » Blog Archive » Lazier functional programming, part 2:

    […] About « Lazier functional programming, part 1 […]

    19 September 2010, 11:36 am

  21. Conal Elliott » Blog Archive » Adding numbers:

    […] Lazier functional programming, part 1 […]

    25 October 2010, 2:44 pm

Leave a comment