[ fix #577 ] generic n-ary functions and products

[gallais]

Comes with documentation of the design decisions!

• (un)curry
• cong, subst
• k-th projections
• hole at position k (cf comment in Generic congN? #577)
• acting on k-th position (both for arrows & product)
• removing k-th element
• adding k-th element
• README module demonstrating how to use all of this

[MatthewDaggitt]

Looks great! I should play around with it a bit and see if I can get any other useful things out. A generalised projection function for products would be incredible...

[gallais]

Come to think of it, Product should probably not be ⊤-terminated if we want
un(curry) to be useful in practice...

Edit: and there's still the case of your hole combinator as well as projections.

[gallais]

Let's also try to give a bunch of examples in a README.X.Y.Z module.

[gallais]

Hmm. I don't think that what I called hole is your notion of hole.
I'm going to drop it for the moment.

FTR:

------------------------------------------------------------------------
-- holeₙ : ∀ n (k : Fin n) →
--         (A₁ → ⋯ Aₙ → B) → Aₖ₊₁ → A₁ → ⋯ → Aₖ → Aₖ₊₂ → ⋯ → Aₙ → B

-- As we have seen earlier, `cong` acts on a function's first variable.
-- If we want to access the second one, we can use `flip`. But what about
-- the fourth one? We typically use an explicit λ-abstraction shuffling
-- variables. Not anymore.

-- Reusing mod-helper just because it takes a lot of arguments:

  hole₁ : ∀ k m n j → mod-helper k m n (j + 1) ≡ mod-helper k m n (suc j)
  hole₁ = λ k m n j → cong {!holeₙ 4 (# 3) mod-helper!} {!!} -- argh!!

Edit: never mind, got it (different definitions).

[gallais]

apologies for taking so long

I don't mind it at all, quite the contrary. I came back to this PR multiple times
since the first time I thought it was ready and fixed / enhanced it in various ways.

[gallais]

It starts to feel like the module should be split up.
The content could be dispatched in:

• Function.Nary
• Relation.Nary (just like we have a lot of combinators in Relation.Unary)
• Data.Product.Nary
• Data.Sum.Nary (TODO)

[JacquesCarette]

This is really wonderful stuff; I agree that the code is getting large, and that splitting things up as you suggest seems like a good idea.

[gallais]

Ok, now that I have shipped my draft about this work (https://gallais.github.io/pdf/tyde19_draft.pdf),
I'll do the split.

[gallais]

I'm annoyed by the module names:

• I like Function.Nary.NonDependent and Relation.Nary
• Data.Product.N-ary.Heterogeneous looks meh

[JacquesCarette]

Why not just Data.Product.N-ary (or Nary)? There is no reason for the Heterogeneous as the homogeneous version is Data.Vec (at Set 'type').

[gallais]

Data.Product.N-ary already exists unfortunately :/

https://agda.github.io/agda-stdlib/Data.Product.N-ary.html

I was tempted to go for Data.Product.Nary.NonDependent to mirror the Function
one but is it not too confusing Nary vs. N-ary?

[JacquesCarette]

I would rename that one Data.Product.N-ary.Fixed (or even FixedN) !

About Nary vs N-ary: I don't really care which is used, consistency is however important. I think it is bad to use both.

[gallais]

If we do not mind a breaking change, we could move the existing
Data.Product.N-ary to e.g. Data.Vec.Recursive and DEPRECATE
the old ones while using Data.Product.Nary.NonDependent for
this work. This would have the added benefit of getting rid of a
bunch of hyphenated modules #265.

[MatthewDaggitt]

Don't have a strong opinion. Happy with whatever you decide!

[gallais]

I thought I had already committed the changes when I decided to amend them. But I
had not so the move + deprecation + renaming is mixed with the merge. Oh well, not
a big deal as we are going to squash everything together anyways.

[JacquesCarette]

By the way, nice TyDe draft. I very much enjoyed reading it.

[gallais]

Thanks!