I'm having difficulty convincing Agda to termination-check the function fmap
below and similar functions defined recursively over the structure of a Trie
. A Trie
is a trie whose domain is a Type
, an object-level type formed from unit, products and fixed points (I've omitted coproducts to keep the code minimal). The problem seems to relate to a type-level substitution I use in the definition of Trie
. (The expression const (μₜ τ) * τ
means apply the substitution const (μₜ τ)
to the type τ
.)
module Temp where
open import Data.Unit
open import Category.Functor
open import Function
open import Level
open import Relation.Binary
-- A context is just a snoc-list.
data Cxt {
The inline/fuse trick can be applied in (perhaps) surprising way. This trick is suited for problems of this sort:
This function is structurally recursive, but in a hidden way.
map
just appliesmap-trie f
to the elements ofxs
, somap-trie
gets applied to smaller (sub-)tries. But Agda doesn't look through the definition ofmap
to see that it doesn't do anything funky. So we must apply the inline/fuse trick to get it past termination checker:Your
fmap
function shares the same structure, you map a lifted function of some sort. But what to inline? If we follow the example above, we should inlinefmap
itself. This looks and feels a bit strange, but indeed, it works:There's another technique you can apply: it's called sized types. Instead of relying on the compiler to figure out when somethig is or is not structurally recursive, you instead specify it directly. However, you have to index your data types by a
Size
type, so this approach is fairly intrusive and cannot be applied to already existing types, but I think it is worth mentioning.In its simplest form, sized type behaves as a type indexed by a natural number. This index specifies the upper bound of structural size. You can think of this as an upper bound for the height of a tree (given that the data type is an F-branching tree for some functor F). Sized version of
List
looks almost like aVec
, for example:But sized types add few features that make them easier to use. You have a constant
∞
for the case when you don't care about the size.suc
is called↑
and Agda implements few rules, such as↑ ∞ = ∞
.Let's rewrite the
Trie
example to use sized types. We need a pragma at the top of the file and one import:And here's the modified data type:
If you leave the
map-trie
function as is, the termination checker is still going to complain. That's because when you don't specify any size, Agda will fill in infinity (i.e. don't-care value) and we are back at the beginning.However, we can mark
map-trie
as size-preserving:So, if you give it a
Trie
bounded byi
, it will give you anotherTrie
bounded byi
as well. Somap-trie
can never make theTrie
larger, only equally large or smaller. This is enough for the termination checker to figure out thatmap (map-trie f) xs
is okay.This technique can also be applied to your
Trie
: