Stream: Coq users

Topic: Operation on Functions


view this post on Zulip James Wood (Jul 19 2022 at 09:26):

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 ns 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.

view this post on Zulip Li-yao (Jul 19 2022 at 18:57):

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 *)

view this post on Zulip Zach Flores (Jul 29 2022 at 15:34):

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.

view this post on Zulip MMY MMY (Jul 29 2022 at 15:38):

Pourriez-vous m'expliquer de quoi s'agit-il?

view this post on Zulip Li-yao (Jul 29 2022 at 16:07):

The idea is that the Class declares a function with a very (overly) general signature compose : d -> c -> r, and Instances 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.

view this post on Zulip Paolo Giarrusso (Jul 29 2022 at 18:50):

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

view this post on Zulip Paolo Giarrusso (Jul 29 2022 at 18:51):

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

view this post on Zulip Zach Flores (Aug 01 2022 at 14:53):

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!

view this post on Zulip Zach Flores (Sep 23 2022 at 15:35):

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.

view this post on Zulip Zach Flores (Sep 23 2022 at 15:37):

Li-yao said:

The idea is that the Class declares a function with a very (overly) general signature compose : d -> c -> r, and Instances 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?

view this post on Zulip Li-yao (Sep 23 2022 at 22:19):

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: Feb 08 2023 at 22:03 UTC