Inline `Data.Vec.Functional.map` for Better Termination Checking

[david-davies]

I ran across an issue with termination checking a recursive function on a data-type using functional vectors, and have simplified to this mwe:

data Stuff (A : Set a) : Set a where
  stuff : (i : ℕ) → Vector (Stuff A) i → Stuff A

mapStuff : (A → B) → Stuff A → Stuff B
mapStuff f (stuff i xs) = stuff i (Vector.map (mapStuff f) xs)

The termination checker gets upset with the call to mapStuff f.
This simplifies to λ x → mapStuff f (xs x), which means the recursive call is smaller, so ideally it should pass the termination check.
Forcing this simplification by adding an inline pragma (without any change to the definition) resolves this:

map2 : (A → B) → ∀ {n} → Vector A n → Vector B n
map2 f xs = f ∘ xs
{-# INLINE map2 #-}

map2Stuff : (A → B) → Foo A → Foo B
map2Stuff f (stuff i xs) = stuff i (map2 (map2Stuff f) xs)

This does rely on _∘_ being inlined also.

[JacquesCarette]

I'm seriously torn about whether to do this. This is obviously a hack to get around a current limitation of Agda, which increases technical debt in stdlib. It also makes goals 'less semantic', which makes writing proofs that are not fragile harder.

I'm not actually saying "don't do this". I think I'm saying we should leave very clear markers in the source code when we choose to do this, so that they are easier to revisit when Agda improves. This particularly one is certainly quite tempting, as I've gotten bit by it too.

[david-davies]

Yeah, it definitely feels like a work-around rather than a solution. I don't have strong feelings on this, I just thought it best to have it written down somewhere should others run into the same issue.

[jamesmckinna]

Thanks @david-davies for the provocation to think... hopefully hard enough to arrive at a sensible resolution of this (kind of) issue.

My sympathies are pretty much with @JacquesCarette , but in some ways, only more so: I think (after what I flatter myself is really quite a lot of thought about this) that part of the problem is the larger issue, long ago identified by Frank Atanassow, of how the very power of types being subject to non-trivial definitional equalities, which leave no trace in the term during typechecking, encourages us both to exploit such power, and abuse it in violating otherwise standard canons about abstraction boundaries, esp. wrt distinguishing specification from implementation... (but there's a separate question, for another time, as to whether access to the power of such non-trivial type equalities means we should reconsider such canons...).

In the context of your issue, I really think that we should not (ever... but) use INLINE pragmas to overcome deficiencies in the already super-complicated typechecking algorithm... with the proviso that actually inlining much of the functionality (sic) in Function.Base (and perhaps only there) does make the otherwise-unbearable bearable.

TL;DR: I think that stdlib should implement things as 'cleanly' as possible subject to the constraints of the typechecker, but offer machine-checked commentary as to what we would, in an ideal world, have wanted to write/have written instead, viz. (spelling things out a bit more verbosely than might be to some people's taste):

module MWE-issue2905 where

open import Data.Nat.Base using (ℕ)
open import Data.Vec.Functional as Vector using (Vector)
open import Function.Base using (_∘_)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

private
  variable
    a b : Level
    A : Set a
    B : Set b
    n : ℕ


data Stuff (A : Set a) : Set a where
  stuff : ∀ (vec : Vector (Stuff A) n) → Stuff A

module MapSpec (f : A → B) where

  map : Stuff A → Stuff B
  map (stuff vec) = stuff (map ∘ vec)

  map-defn : ∀ vec → map (stuff {n = n} vec) ≡ stuff (Vector.map map vec)
  map-defn vec = refl

The definition (sic) of map happily typechecks under v2.8.0 (albeit thanks to the inlining of _∘_; otherwise you would have to go the whole hog and do so by hand), while the normaliser has no problem checking map-defn that definitionally, this map is in fact, identical to the intended would-be definiens as map (stuff {n = n} vec) = stuff (Vector.map map vec).

So the 'implementation' may not be the intended 'specification' here, even though they are, in fact, identical ;-)

A satisfactory solution?

I'm not sure, but at least it seems to be one which is cognate with the other 'standard' FP examples in stdlib where eg implementing functions on lists via the generic combinators foldr/foldl are in fact propositionally equal to their direct recursive definitions.

PS. Presumably also the term map-defn would further licence, directly, turning that equation into a rewrite rule, but again as @JacquesCarette points out, appeals to such pragmas potentially makes code less robust (or at least, might give rise to non-local fragiity downstream... not sure I'm quite across all the consequences of using rewrites in Agda, so it seems safer to avoid having to think about such things!)