Hello all, this is my first post on the Zulip (not sure if I really need to announce that, but would like everyone to know I'm new to this). Let me first describe what we would really like to implement mathematically:

Let's assume all the $c_i, b_j,$ and $d$ live in `Set`

.

$f : c_1 \rightarrow \ldots \rightarrow c_n \rightarrow d$

$g : b_1 \rightarrow \ldots \rightarrow b_m \rightarrow c_i$

We want to construct a function in Coq with all this information, called $f \circ_i g$ such that

$f\circ_i g : c_1 \rightarrow\cdots c_{i-1} \rightarrow b_1\rightarrow\cdots \rightarrow b_m\rightarrow c_{i+1}\rightarrow\cdots\rightarrow c_n\rightarrow d$

and

$z_1 : c_1,\ldots, z_{i-1}: c_{i-1}, z_i : b_1,\ldots, z_{i+m-1} : b_m, z_{i+m} : c_{i+1},\ldots, z_{n+m-1} : c_n$

And

$(f\circ_i g) (z_1,\ldots, z_{i+m-1}) = f(z_1,\ldots, z_{i-1}, g (z_i,\ldots, z_{i+m-1}), z_{i+m},\ldots , z_{n+m-1})$

So our current attempt to do this was to do what I thought was the obvious thing: Define heterogeneous lists in Coq, and then make a definition of this that involved a bunch of removing, inserting and keeping the correct members of the heterogeneous list. This turns out to be a type casting nightmare, and is generally really ugly. It also needs to come with with several hypotheses about the size of the lists involved.

Another unfortunate consequence of choices that were made in this direction requires us to define hom sets in this setting as:

```
Definition homSet (d : Set)(c : list Set) : Type :=
hList c -> d.
```

Where `hList c`

is the type of all heterogeneous lists that can be made from the list `c`

. This carries with it the difficulty in defining the identity function, among other problems.

In order to remedy the situation, and wanting to avoid defining new types, we'd really like to perform operations analogous to some of the stuff in the n-ary library, though probably a little different. We start with an analogue of `nfun`

for lists:

```
Fixpoint listFun (B:Set)(l: list Set) :=
match l with
| [] => B
| h::t => h -> listFun B t
end.
Notation " l --> B " := (listFun B l)
(at level 50) : type_scope.
```

Now remember our goal is, given

```
Definition lookupSet (i: nat)(xs : list Set) : Set :=
nth i xs unit.
Definition insert{A : Type} (i:nat) (old new : list A) : list A :=
firstn i old ++ new ++ skipn (i+ 1) old.
f: c --> d
g: b--> ci
lookupSet i c = ci
```

we want to obtain a function

```
circ i f g : insert i c b --> d
```

Currently trying to understand the Coq n-ary library in hopes that it gives us a direction on how to do this, but don't have a lot of ideas at the moment, so any help (or ideas!) would be greatly appreciated.

My intuition would be to define a family `Elem {A : Type} : A -> list A -> Set`

of proof-relevant locations in a list, and use a bit of automation to generate inhabitants of it from the list and a natural number (essentially a beefed-up version of how you can generate `Fin.t n`

s by providing an `m`

and checking that `ltb m n`

evaluates to `true`

). From an `Elem X old`

, you should be able to read off the relevant portions of `old`

and splice `new`

in in a controlled way.

The Haskell way (with type classes):

```
(* f : c1 -> ... -> cn -> d
g : b1 -> ... -> bm -> ci
f .i g : c1 -> ... -> c(i-1)
-> b1 -> ... -> bm
-> ci+1 -> ... -> cn -> d *)
Class Compose (i : nat) (d c r : Type) : Type :=
compose : d -> c -> r.
#[global]
Instance Compose_S n c0 d c r `{Compose n d c r}
: Compose (S n) (c0 -> d) c (c0 -> r) :=
fun f g x0 => compose (f x0) g.
#[global]
Instance Compose_0_c c0 d b c r `{Compose 0 (c0 -> d) c r}
: Compose 0 (c0 -> d) (b -> c) (b -> r) :=
fun f g x0 => compose f (g x0).
#[global]
Instance Compose_0 d c : Compose 0 (c -> d) c d :=
fun f g => f g.
Arguments compose : clear implicits.
Arguments compose i {d c r _} _ _.
Parameter c : nat -> Type.
Parameter b : nat -> Type.
Parameter f : c 1 -> c 2 -> c 3 -> c 4 -> nat.
Parameter g : b 1 -> b 2 -> b 3 -> c 2.
Check compose 1 f g.
(* compose 1 f g : c 1 -> b 1 -> b 2 -> b 3 -> c 3 -> c 4 -> nat *)
```

Li-yao said:

The Haskell way (with type classes):

`(* f : c1 -> ... -> cn -> d g : b1 -> ... -> bm -> ci f .i g : c1 -> ... -> c(i-1) -> b1 -> ... -> bm -> ci+1 -> ... -> cn -> d *) Class Compose (i : nat) (d c r : Type) : Type := compose : d -> c -> r. #[global] Instance Compose_S n c0 d c r `{Compose n d c r} : Compose (S n) (c0 -> d) c (c0 -> r) := fun f g x0 => compose (f x0) g. #[global] Instance Compose_0_c c0 d b c r `{Compose 0 (c0 -> d) c r} : Compose 0 (c0 -> d) (b -> c) (b -> r) := fun f g x0 => compose f (g x0). #[global] Instance Compose_0 d c : Compose 0 (c -> d) c d := fun f g => f g. Arguments compose : clear implicits. Arguments compose i {d c r _} _ _. Parameter c : nat -> Type. Parameter b : nat -> Type. Parameter f : c 1 -> c 2 -> c 3 -> c 4 -> nat. Parameter g : b 1 -> b 2 -> b 3 -> c 2. Check compose 1 f g. (* compose 1 f g : c 1 -> b 1 -> b 2 -> b 3 -> c 3 -> c 4 -> nat *)`

Oh, wow. That is exactly what I wanted. Several of us were really struggling with this for a long time. Would you mind walking me through how this works? I am mathematician and not a functional programmer.

(deleted)

The idea is that the `Class`

declares a function with a very (overly) general signature `compose : d -> c -> r`

, and `Instance`

s define inference rules such that `Compose i d c r`

is derivable exactly when the type `d -> c -> r`

has a shape matching your desired `.i`

operator.

I was wondering: this is useful, but it does not implement \ring_i as a function of i, only concrete instances for the indexes needed in your program

Is this sufficient for @Zach Flores 's original request? That's not obvious...

Paolo Giarrusso said:

I was wondering: this is useful, but it does not implement \ring_i as a function of i, only concrete instances for the indexes needed in your program

I will say that it definitely seems a step in the right direction. I'm going to say this definitely seems to help, and going to see how sufficient it is. I'll keep everyone posted!

I have been curious if this can be made into something using inductive types. It's not hard to make a function that does this for types (this is just some list insertion), but we don't know how to do this without making some kind of crazy thing using heterogeneous lists. Even then, it's a mess of parameters and I haven't gone back and tried to create a concrete example.

Any thoughts on this would be really appreciated.

Li-yao said:

The idea is that the

`Class`

declares a function with a very (overly) general signature`compose : d -> c -> r`

, and`Instance`

s define inference rules such that`Compose i d c r`

is derivable exactly when the type`d -> c -> r`

has a shape matching your desired`.i`

operator.

Is there any way to do this without type classes?

Lucky for you, I've been practicing Agda. Note there is a slight simplification you can do, which removes the parameter n: use (ci+1 -> ... -> cn -> d) as d. In hindsight, this simplification probably allows this implementation to be rewritten with lists instead of vectors.

```
From Equations Require Import Equations.
From Coq Require Import Vector.
Notation "[]" := (Vector.nil _) : vector_scope.
Notation "t :: ts" := (Vector.cons _ t _ ts) : vector_scope.
Infix "^" := Vector.t.
#[local] Open Scope vector_scope.
Equations arr {n : nat} (ts : Type ^ n) (t' : Type) : Type :=
arr [] t' := t' ;
arr (t :: ts) t' := t -> arr ts t'.
Equations compose' {m : nat} (bs : Type ^ m) {ci d : Type} : (ci -> d) -> arr bs ci -> arr bs d :=
compose' [] f g := f g ;
compose' (b :: bs) f g := fun x => compose' bs f (g x).
(* f : c0 -> ... -> cn-1 -> cn -> d (* NB: d itself may be a function type *)
g : b0 -> ... -> bm -> cn
compose cs bs f g : c0 ... cn-1 b0 ... bm -> d
*)
Equations compose {n m : nat} (cs : Type ^ n) {ci d : Type} (bs : Type ^ m)
: arr cs (ci -> d) -> arr bs ci -> arr cs (arr bs d) :=
compose [] bs f g := compose' bs f g ;
compose (c :: cs) bs f g := fun x => compose cs bs (f x) g.
(* Infer the lists from the types *)
Class Split (T : Type) (i : nat) (Args : Type ^ i) (d : Type) : Prop :=
Split_eq : arr Args d = T.
#[global] Instance Split_S {B n A As d} {e : Split B n As d}
: Split (A -> B) (S n) (A :: As) d :=
match e with
| eq_refl => eq_refl
end.
#[global] Instance Split_O A : Split A O [] A := eq_refl.
Definition compose_ (i : nat) {cs : Type ^ i} {m} {bs : Type ^ m} {ci d cd bc : Type}
{ec : Split cd i cs (ci -> d)} {eb : Split bc m bs ci} : cd -> bc -> arr cs (arr bs d) :=
let 'eq_refl := ec in
let 'eq_refl := eb in compose cs bs.
Section Example.
Context (c : nat -> Type) (b : nat -> Type) (d : Type).
Context (f : c 0 -> c 1 -> c 2 -> d).
Context (g : b 0 -> b 1 -> c 1).
(* Without the class, we must provide the list of types. *)
Definition fg := compose (c 0 :: []) (b 0 :: b 1 :: []) f g.
Definition type_of {A : Type} (_ : A) : Type := A.
Compute (type_of fg).
(* With the class, the lists of types can be inferred. *)
Definition fg' := compose_ 1 f g.
Compute (type_of fg').
End Example.
```

Last updated: Jun 24 2024 at 12:02 UTC