Bushtree and GNDT

[mmontin]

We want to make an instantiation of BushTrees as GNDT.

[pedagand]

And then look at what would happen if we tried to turn it into an iterative #3 definition. (cf. #5)

[pedagand]

Nope, won't work as-is with BushTrees.

Currently, we have

data GNDT {a} (Σ : SIG)(F : TT)(A : Set a) : Set a where
  ctor : ⟦ Σ ⟧ A (GNDT Σ F (F A)) → GNDT Σ F A

where F is a pre-existing functor which we compose as we add ctors.

BushTree is defined by

data Bush {a} : Set a → Set a where
  bnil : {A : Set a} → Bush A
  bcons : {A : Set a} → A → Bush (Bush A) → Bush A

which means that F would need to be defined in terms of Bush whilst we are defining the GNDT corresponding to Bush:

ΣBush : SIG
ΣBush = `⊤ `⊎ (`A `× `X)

Bush : ∀ {a} → Set a → Set a
Bush A = GNDT0 ΣBush Bush A

The termination checker is very unhappy with this definition.

There might be ways to re-generalize the definition of GNDT to allow for this pattern, a quick attempt did not yield convincing results.

[pedagand]

Section 5.3 "First-order vs. higher-order nested types" of Numerical Representations as Higher-Order Nested Datatypes explains to lift first-order nested types (such as Bush above) to higher-order ones.

This section suggests that it is not too difficult to (manually, at least) work with higher-order definitions only. For example, Bush tree would be:

data BushR bush a =
  | BCons (BushR (Fork bush) a)
  | BNil (bush a)
data Bush = BushR Id a

Fork and Id could be expressed as SIG, which is closed under composition so there is some hope that it works.

[pedagand]

Other example:

First-order:

  data Fork bush = bush × bush

  data RandomAccessList bush =
   | Nil
   | One bush (RandomAccessList (Fork bush))
   | Two (Fork bush) (RandomAccessList (Fork bush))

  data IxSequence a = RandomAccessList a

Higher-order:

  data RandomAccessList' bush a =
  | Nil
  | One (bush a) (RandomAccessList' (Fork bush) a)
  | Two (Fork bush a) (RandomAccessList' (Fork bush) a)

  data Id a = Id a
  data IxSequence a = RandomAccessList' Id a

We have:

RandomAccessList a  = RandomAccessList' Id a
RandomAccessList' bush a = RandomAccessList (bush a)