Representations of execution traces

So far the clearest general principle arising from the binomial tabulation story is the interpretation of inhabitants of indexed datatypes as execution traces of nondeterministic functions — that is, relations. It’s been well known that inductively defined relations —or logic programs— can be expressed as indexed datatypes. For example, we can define the relation that maps a list to one of its prefixes as a datatype

data Init {A : Set} : List A → List A → Set where
  nil       :              Init []       []
  cons-nil  :              Init (x ∷ xs) []
  cons-cons : Init xs ys → Init (x ∷ xs) (x ∷ ys)

which directly corresponds to a logic program, with the three constructors corresponding to the clauses of the logic program. The logic program is executed by (implicitly) constructing derivations using the clauses, and such derivations can be thought of as execution traces.

But there is more than one way to represent execution traces. Another way is to introduce a continuation and allow execution traces to be concatenated:

data InitC {A : Set} (P : List A → Set) : List A → Set where
  nil       : P []                  → InitC P []
  cons-nil  : P []                  → InitC P (x ∷ xs)
  cons-cons : InitC (P ∘ (x ∷_)) xs → InitC P (x ∷ xs)

For Init, an execution trace ends with nil or cons-nil, whereas for InitC, a nil or cons-nil constructor contains a further execution trace specified by the continuation P. For example, we can similarly define the suffix relation as

data TailC {A : Set} (P : List A → Set) : List A → Set where
  nil         : P []       → TailC P []
  cons-whole  : P (x ∷ xs) → TailC P (x ∷ xs)
  cons-proper : TailC P xs → TailC P (x ∷ xs)

and then define the segment relation by function composition (rather than relation composition!):

SegC : {A : Set} (P : List A → Set) → List A → Set
SegC = InitC ∘ TailC

I’m still baffled about whether P can legitimately be called a continuation (or more generally, what this construction is mathematically), although the idea seems to be essentially the same as continuation-passing style: an ordinary function computes a result and ends its execution, whereas its continuation-passing version passes the result to a continuation, and therefore specifies only an initial portion of its execution, with the rest of the execution abstracted as the continuation.

Logically, InitC existentially quantifies over execution traces and results — InitC P xs is isomorphic to Σ[ ys ∈ List A ] Init xs ys × P ys. However, compared to the latter representation as a tuple, InitC is actually less convenient to use because the result ys and the proof of type P ys are hidden at the end of the execution trace and cannot be accessed directly. Moreover, if we want to perform induction on InitC, we can do it on Init as well. So InitC doesn’t seem to have any advantage over the tuple representation, and for convenience we redefine it as a record:

record InitC {A : Set} (P : List A → Set) (xs : List A) : Set where
  constructor initC
  field
    {prefix} : List A
    isPrefix : Init xs prefix
    payload  : P prefix

Things seem to become more interesting if we consider an inductive representation of universal quantification over execution traces and results: (ys : List A) → Init xs ys → P ys. Instead of representing just one execution trace, we can represent all possible execution traces as a tree, which branches whenever there’s a nondeterministic choice. For Init, such trees can be defined as

data Inits {A : Set} (P : List A → Set) : List A → Set where
  [_] : P []                         → Inits P []
  _∷_ : P [] → Inits (P ∘ (x ∷_)) xs → Inits P (x ∷ xs)

This representation is first-order, so it’s at least markedly different from the higher-order/functional representation and worth considering. The binomial tabulation story shows that this is the design principle underlying Richard Bird’s use of binary/binomial trees. The principle seems general enough, and there should be other examples.

A natural place to find more examples is optimisation problems, which involve universal quantification over candidate solutions. For example, in the maximum prefix sum problem, we can use Inits to represent all the prefix sums of an input list (from which we’ll choose a maximum later): defining

record Exactly {A : Set} (x : A) : Set where
  constructor exactly
  field
    payload      : A
    {{equality}} : payload ≡ x

to attach an equality constraint to a value, we can write a function inits to compute all the prefixes

inits : (xs : List A) → Inits Exactly xs
inits []       = [ exactly [] ]
inits (x ∷ xs) = exactly [] ∷ mapInits (mapExactly (x ∷_)) (inits xs)

and then, assuming a type Val : Set that supports addition, compose inits with ‘map sum’ to compute all the prefix sums:

prefixSums : (xs : List Val) → Inits (Exactly ∘ sum) xs
prefixSums = mapInits (mapExactly sum) ∘ inits

Alternatively, we can directly write

prefixSums' : (xs : List Val) → Inits (Exactly ∘ sum) xs
prefixSums' []       = [ exactly zero ]
prefixSums' (x ∷ xs) = exactly zero
                     ∷ mapInits (mapExactly (x +_)) (prefixSums' xs)

which can be seen to be the result of fusing ‘map sum’ into inits. The development is minimal but looks nice so far: The specification is encoded as a precise type that nevertheless can have different implementations, so the type isn’t over-specifying too much. There’s not much overhead to write the precisely typed programs (compared to writing simply typed ones). What I find particularly interesting is that the correctness of prefixSums' used to be established with respect to prefixSums by fold fusion in a simply typed setting, whereas here the correctness is established solely by typing. This means that we can write prefixSums' directly and still make sure it’s correct without going through a derivation, which can be tedious especially when the program to write is obvious. On the other hand, program derivation techniques —in particular more powerful theorems like those dealing with optimisation problems in the later sections of the Algebra of Programming book— will still be useful when the program to write is not obvious. The point, as always, is to be able to skip boring steps and concentrate on where ingenuity is required.

One can argue that the type used above

IndPrefixSums : Set
IndPrefixSums = (xs : List Val) → Inits (Exactly ∘ sum) xs

is still over-specifying because it requires the prefix sums to be returned in a non-empty list and in a specific order, and that a more adequate specification is

PrefixSums : Set
PrefixSums = (xs ys : List Val) → Init xs ys → Exactly (sum ys)

because it only requires that we can get every prefix sum through a functional interface without saying anything about the internals of the function. That is, it makes more sense to start from PrefixSums as the specification, and then make a choice to switch to IndPrefixSums to use a non-empty list to represent all the prefix sums, formally by applying

fromInits : Inits P xs → (ys : List A) → Init xs ys → P ys
fromInits [ p ]    _  nil          = p
fromInits (p ∷ ps) _  cons-nil     = p
fromInits (p ∷ ps) _ (cons-cons i) = fromInits ps _ i

which fits the inductive representation into the functional interface, and can be thought of as the soundness of Inits (correctly implementing the universal quantification). A persisting problem in traditional functional program derivation is that functional specifications can seriously affect the result of derivations and need to be chosen carefully. I think this shows that such ‘specifications’ are not starting points but actually intermediate stops, to arrive at which some reasoning steps need to have already been taken. The Algebra of Programming book proposed to start from relations as specifications and then refine them to functions as implementations, but the relation calculus is too complicated and difficult to master. (Even Shin, who has worked with the relation calculus extensively, admits that he has to look up definitions and laws frequently.) By contrast, dependent types work nicely as specifications because they include a straightforward logical language, and it’s easier to refine them to more detailed types (by writing and applying fromInits, for example) and eventually to functions thanks to the Curry-Howard intuition. One could argue that relational definitions could still be expanded and reasoned about set-/type-theoretically, but the results of expansion tend to be obscure and tedious to manipulate. I think it should be the other way around: we work in the Curry–Howard way by default, and introduce relational abstractions where suitable.

Unfortunately, the ‘maximum’ part in maximum prefix sum seems to get messier. My idea is that maximum can be implemented for non-empty lists whose elements have a decidable total ordering; then, Inits is an ornamentation of non-empty lists, so we should be able to just lift maximum for non-empty lists to work on Inits. Sadly, such lifting is still not available more than a decade after the invention of ornaments, so for now we have to implement maximum for Inits manually. The element types in Inits are from a type family, and the decidable total ordering needs to make sense between possibly different types from the same family:

record MaxFam {A : Set} (P : A → Set) : Set₁ where
  constructor maxFam
  field
    _≤_     : ∀ {x y} → P x → P y → Set
    ≤-refl  : ∀ {x} {p : P x} → p ≤ p
    ≤-trans : ∀ {x y z} {p : P x} {q : P y} {r : P z}
            → p ≤ q → q ≤ r → p ≤ r
    ≤-dec   : ∀ {x y} (p : P x) (q : P y) → p ≤ q ⊎ q ≤ p

My implementation of maximum for Inits isn’t particularly pleasing:

maxInits : {P : List A → Set} (mf : MaxFam P) → let open MaxFam mf in
           Inits P xs → Σ[ (initC _ q) ∈ InitC P xs ]
                        Inits (λ ys → Σ[ p ∈ P ys ] p ≤ q) xs
maxInits mf [ p ]    = initC nil p , [ (p , mf .MaxFam.≤-refl) ]
maxInits mf (p ∷ ps) with maxInits (MaxFam-fun (_ ∷_) mf) ps
maxInits mf (p ∷ ps) | initC i q , ps' with mf .MaxFam.≤-dec p q
maxInits mf (p ∷ ps) | initC i q , ps' | inj₁ p≤q =
  initC (cons-cons i) q , (p , p≤q) ∷ ps'
maxInits mf (p ∷ ps) | initC i q , ps' | inj₂ q≤p =
  initC cons-nil p , (p , mf .MaxFam.≤-refl) ∷
                     mapInits (map₂ (flip (mf .MaxFam.≤-trans) q≤p)) ps'

Usually, the type of maximum should be a dependent function type saying that the output is an element of the input list that’s greater than all the elements of the list. This could be stated by instantiating the generic All construction applied to Inits, but I fear that stacking constraints on a datatype would make it too complicated. In this case, if P has been made precise enough such that we only need to care about the existence of inhabitants and not about which particular inhabitants are exhibited, then we can simply produce another Inits that only imposes more constraints on its elements and doesn’t insist that the elements are the input ones. For example, for maximum prefix sum P is Exactly ∘ sum, and the family of types are uniquely inhabited (and thus extremely precise). Through Curry–Howard, ‘imposing more constraints’ means pairing with proofs, and I like how maxInits returns the input list with elements augmented with proofs as we know more about the ordering among those elements — that is, knowledge is reified as proofs. What I don’t like is that the Agda definition looks messy somehow, and in particular it looks inconvenient for equational reasoning. I’m not sure exactly what’s wrong though.

Back to maximum prefix sum, for which we can give a specification

MaxPrefixSum : Set
MaxPrefixSum = (xs : List Val)
             → Σ[ m ∈ Val ] Σ[ ys ∈ List Val ]
               Init xs ys × m ≡ sum ys ×
               ((zs : List Val) → Init xs zs → sum zs ≤ m)

and refine it to a type with InitC and Inits:

IndMaxPrefixSum : Set
IndMaxPrefixSum =
    (xs : List Val)
  → Σ[ (initC _ (exactly m)) ∈ InitC (Exactly ∘ sum) xs ]
    Inits (λ ys → Σ[ (exactly n) ∈ Exactly (sum ys) ] n ≤ m) xs

This type can again be implemented by either a composition of existing functions or a direct definition:

maxPrefixSum : IndMaxPrefixSum
maxPrefixSum = maxInits (MaxFam-fun sum (MaxFam-Exactly MaxFam-Val))
             ∘ mapInits (mapExactly sum) ∘ inits

maxPrefixSum' : IndMaxPrefixSum
maxPrefixSum' [] = initC nil (exactly zero) , [ (exactly zero , ≤-refl) ]
maxPrefixSum' (x ∷ xs) with maxPrefixSum' xs
maxPrefixSum' (x ∷ xs) | initC i (exactly m) , ps with ≤-dec (x + m) zero
maxPrefixSum' (x ∷ xs) | initC i em , ps | inj₁ x+m≤0 =
  initC cons-nil (exactly zero) ,
  (exactly zero , ≤-refl) ∷ mapInits (map-Σ (mapExactly (x +_)) (flip ≤-trans x+m≤0 ∘ +-mono-r x)) ps
maxPrefixSum' (x ∷ xs) | initC i em , ps | inj₂ 0≤x+m =
  initC (cons-cons i) (mapExactly (x +_) em) ,
  (exactly zero , 0≤x+m) ∷ mapInits (map-Σ (mapExactly (x +_)) (+-mono-r x)) ps

The direct definition maxPrefixSum' looks even messier. I can still roughly see and imagine that this is the result of fusing maxInits with prefixSums', but I can’t imagine actually doing the fusion. Another messy definition is the soundness of IndMaxPrefixSum:

IndMaxPrefixSum-soundness : IndMaxPrefixSum → MaxPrefixSum
IndMaxPrefixSum-soundness f xs =
  let (initC {ys} i (exactly m {{meq}}) , ps) = f xs
  in  m , ys , i , meq , λ zs j → see-below zs (fromInits ps zs j)
  where
    see-below : {m : Val} (zs : List Val)
              → Σ[ (exactly n) ∈ Exactly (sum zs) ] n ≤ m → sum zs ≤ m
    see-below _ (exactly _ {{refl}} , ineq) = ineq

This might be argued to be either a success or a failure of the Curry–Howard paradigm — you don’t have to think much to prove this, but the only interesting bit, which is the use of fromInits, is buried deep in boring details for restructuring the proofs. There doesn’t seem to be a fundamentally better way though — if we were working in relation calculus, we would use point-free combinators to do something similar, which I think is just harder. Perhaps the best way to think about this is that this kind of proof is simply trivial and should be automatically synthesised and then ignored by the programmer (who only verifies it intuitively).

An important question that should be asked is whether it’s beneficial to introduce Inits into this development — what if we directly implement MaxPrefixSum rather than refine it to IndMaxPrefixSum?

maxPrefixSum'' : MaxPrefixSum
maxPrefixSum'' [] = zero , _ , nil , refl , λ { _ nil → ≤-refl }
maxPrefixSum'' (x ∷ xs) with maxPrefixSum'' xs
maxPrefixSum'' (x ∷ xs) | m , _ , i , meq , f with ≤-dec (x + m) zero
maxPrefixSum'' (x ∷ xs) | m , _ , i , meq , f | inj₁ x+m≤0 =
  zero , _ , cons-nil , refl ,
  λ { _ cons-nil → ≤-refl; _ (cons-cons j) → ≤-trans (+-mono-r x (f _ j)) x+m≤0 }
maxPrefixSum'' (x ∷ xs) | m , ys , i , meq , f | inj₂ 0≤x+m =
  (x + m) , _ , cons-cons i , cong (x +_) meq ,
  λ { _ cons-nil → 0≤x+m; _ (cons-cons j) → +-mono-r x (f _ j) }

This doesn’t look bad — in particular we get to omit all the maps. Shin suspects that the functional representation would be inefficient in practice though. Theoretically, I suspect that the functional representation doesn’t really support induction, particularly after a discussion with Zhixuan. It should be worthwhile to do a more systematic comparison, but not in this post.

One last thing that I should mention is that this isn’t actually the kind of development I wanted to try in the first place. I was hoping that by relating datatypes to relations, I could do some form of ‘datatype derivation’ by importing relational derivation techniques, but I end up discussing fusion still at the program level. That is, what I really want is a ‘datatype calculus’ that helps us to design highly customised indexed datatypes for intrinsically typed programming. Maximum prefix sum doesn’t seem to be a good example because the result is just a value rather than an inhabitant of a datatype into which we can embed constraints. (On the other hand, if we also take into account the output proof that the result is maximum, that can still be expressed as a datatype. But somehow I end up just reusing Inits…) I reckon I’m still very far away from my goal.

Agda file: MPS.agda