## 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.,

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:

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’ »