## Memoizing polymorphic functions via unmemoization

Last year I wrote two posts on memoizing polymorphic functions. The first post gave a solution of sorts that uses a combination of patricia trees (for integer-keyed maps), stable names, and type equality proofs. The second post showed how to transform some functions that do not quite fit the required form so that they do fit.

Dan Piponi wrote a follow-up post Memoizing Polymorphic Functions with High School Algebra and Quantifiers showing a different approach that was more in the spirit of type-directed functional memoization, as it follows purely from mathematical properties, free of the deeply operational magic of stable names. Recently, I finally studied and worked with Dan’s post enough to understand what he did. It’s very clever and beautiful!

This post re-presents Dan’s elegant insight as I understand it, via some examples that helped it come together for me.

Continue reading ‘Memoizing polymorphic functions via unmemoization’ »

## Fixing broken isomorphisms — details for non-strict memoization, part 2

The post Details for non-strict memoization, part 1 works out a systematic way of doing non-strict memoization, i.e., correct memoization of non-strict (and more broadly, non-hyper-strict) functions. As I mentioned at the end, there was an awkward aspect, which is that the purported “isomorphisms” used for regular types are not quite isomorphisms.

For instance, functions from triples are memoized by converting to and from nested pairs:

```untriple ∷ (a,b,c) -> ((a,b),c)
untriple (a,b,c) = ((a,b),c)

triple ∷ ((a,b),c) -> (a,b,c)
triple ((a,b),c) = (a,b,c)```

Then `untriple` and `triple` form an embedding/projection pair, i.e.,

```triple ∘ untriple ≡ id
untriple ∘ triple ⊑ id```

The reason for the inequality is that the nested-pair form permits `(⊥,c)`, which does not correspond to any triple.

`untriple (triple (⊥,c)) ≡ untriple ⊥ ≡ ⊥`

Can we patch this problem by simply using an irrefutable (lazy) pattern in the definition of `triple`, i.e., `triple (~(a,b),c) = (a,b,c)`? Let’s try:

`untriple (triple (⊥,c)) ≡ untriple (⊥,⊥,c) ≡ ((⊥,⊥),c)`

So isomorphism fails and so does even the embedding/projection property.

Similarly, to deal with regular algebraic data types, I used a class that describes regular data types as repeated applications of a single, associated pattern functor (following A Lightweight Approach to Datatype-Generic Rewriting):

```class Functor (PF t) ⇒ Regular t where
type PF t ∷ * → *
unwrap ∷ t → PF t t
wrap   ∷ PF t t → t```

Here `unwrap` converts a value into its pattern functor form, and `wrap` converts back. For example, here is the `Regular` instance I had used for lists:

```instance Regular [a] where
type PF [a] = Const () :+: Const a :*: Id

unwrap []     = InL (Const ())
unwrap (a:as) = InR (Const a :*: Id as)

wrap (InL (Const ()))          = []
wrap (InR (Const a :*: Id as)) = a:as```

Again, we have an embedding/projection pair, rather than a genuine isomorphism:

```wrap ∘ unwrap ≡ id
unwrap ∘ wrap ⊑ id```

The inequality comes from ⊥ values occurring in `PF [a] [a]` at type `Const () [a]`, `()`, `(Const a :*: Id) [a]`, `Const a [a]`, or `Id [a]`.

Continue reading ‘Fixing broken isomorphisms — details for non-strict memoization, part 2’ »

## Lazier functional programming, part 2

In Lazier functional programming, part 1, I suggested that some of the standard tools of lazy functional programming are not as lazy as they might be, including even `if-then-else`. Generalizing from boolean conditionals, I posed the puzzle of how to define a lazier `either` function, which encapsulates case analysis for sum types. The standard definition:

```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```

The comments to part 1 fairly quickly converged to something close to the laxer definition I had in mind:

`eitherL f g = const (f ⊥ ⊓ g ⊥) ⊔ either f g`

which is a simple generalization of Luke Palmer‘s laxer if-then-else (reconstructed from memory):

`bool c a b = (a ⊓ b) ⊔ (if c then a else b)`

Continue reading ‘Lazier functional programming, part 2’ »

## Lazier functional programming, part 1

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?

Continue reading ‘Lazier functional programming, part 1’ »

## “Everything is a function” in Haskell?

There a belief about Haskell that keeps popping up in chat rooms and mailing lists — one that I’ve been puzzling over for a while. One expression of the belief is “everything is a function” in Haskell.

Of course, there are all of these non-functions that need to be accounted for, including integers, booleans, tuples, and lists. What about them? A recurring answer is that such things are “functions of no arguments” or functions of a one-element type or “constant functions”.

I wonder about how beliefs form, spread, and solidify, and so I asked around about how people came to this notion and how they managed to hold onto it. I had a few conjectures in mind, which I kept to myself to avoid biasing people’s responses. Of the responses I got, some were as I’d imagined, and some were quite surprising to me, revealing some of my blind spots about others’ thinking and about conversation dynamics.

My thanks to the many Haskellers, especially newbies, who took the time to help me understand their thought processes. If you’re interested and in a patient mood, you can see the unedited responses on a Haskell reddit thread and on a #haskell IRC log. There were also a few responses on Twitter.

Edits:

• 2009-08-04: Added “simplify”: “Would making everything a function really simplify the formal system that is Haskell programming?”. Thanks, SLi.
• 2009-08-04: Focus on “constant function” story for “It makes things simpler”. I realized that I hadn’t said what I intended there. Thanks, Jonathan Cast.
• 2011-03-04: Remarks on mutability & dynamic typing, under “Operational thinking”

## Topless data

Functional programming abounds with recursively defined data types. We often draw these structured values as trees with the root at the top and the leaves at the bottom. Lazy functional programming allows values (structures) of these types to be “bottomless”, meaning we can descend forever. There are many examples of how supporting such values gives an enormous boost to modularity. (See, e.g., John Hughes’s classic paper Why Functional Programming Matters.) We usually refer to these values as “infinite”, but I’d like to suggest “bottomless” as a more specific alternative, and to point out a limitation that perhaps is not widely noticed.

Although we can descend infinitely in lazy functional programming, we can only ascend finitely. If I’m traversing a lazy list, there may be infinitely many elements on my right (yet to be visited) but only finitely many on my left (already visited). While traversing a tree, there may be infinite paths below but only a finite one above (leading to my current position).

In other words, our data is bottomless, but not topless. What would it be like to go beyond our usual merely uni-infinite data and program with bi-infinite data instead? With data that is both bottomless and topless?

## Another angle on zippers

The zipper is an efficient and elegant data structure for purely functional editing of tree-like data structures, first published by Gérard Huet. Zippers maintain a location of focus in a tree and support navigation operations (up, down, left, right) and editing (replace current focus).

The original zipper type and operations are customized for a single type, but it’s not hard to see how to adapt to other tree-like types, and hence to regular data types. There have been many follow-up papers to The Zipper, including a polytypic version in the paper Type-indexed data types.

All of the zipper adaptations and generalizations I’ve seen so far maintain the original navigation interface. In this post, I propose an alternative interface that appears to significantly simplify matters. There are only two navigation functions instead of four, and each of the two is specified and implemented via a fairly simple one-liner.

I haven’t used this new zipper formulation in an application yet, so I do not know whether some usefulness has been lost in simplifying the interface.

The code in this blog post is taken from the Haskell library functor-combo and completes the `Holey` type class introduced in Differentiation of higher-order types.

Edits:

• 2010-07-29: Removed some stray `Just` applications in `up` definitions. (Thanks, illissius.)
• 2010-07-29: Augmented my complicated definition of `tweak2` with a much simpler version from Sjoerd Visscher.
• 2010-07-29: Replaced `fmap (first (:ds'))` with `(fmap.first) (:ds')` in `down` definitions. (Thanks, Sjoerd.)

Continue reading ‘Another angle on zippers’ »