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)
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 (~(a,b),c) = (a,b,c)?
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
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
Continue reading ‘Fixing broken isomorphisms — details for non-strict memoization, part 2’ »