I've been looking at free functors again and I had an idea inspired by call by push value and substructural logic.
Given a category $\text C$, instead of just creating a free functor $\text{F}: \text{Set} \rightarrow \text C$ is there a reasonable notion of free asymmetric tensor $\otimes : \text{Set} \times \text C \rightarrow \text C$ ?
My intuition is that if you think of a free functor as a monad and then as an effect system it's natural to ask if you can think of the same idea but in terms of substructural logic.
I think the appropriate laws assuming a terminal object $\text{i} \in \text C$ would include:
$$\text{F} = - \otimes \text{i}$$
Associativity
$$ \text{assoc}: x \otimes y \otimes z \leftrightarrow (x \times y) \otimes z $$
Left unit
$$ \text{lunit}: \cdot \otimes x \leftrightarrow x$$
I tried playing around a bit with the idea but I think I need help.
I think I want to think of the free functor to the category of endofunctors over $\text C$?
Require Import Coq.Unicode.Utf8.
Require Import Coq.Setoids.Setoid.
Require Import Coq.Classes.SetoidClass.
Module Import Term.
Class Term := {
T: Type ;
Term_Setoid: Setoid T ;
one: T ;
zero: T ;
prod: T → T → T ;
sum: T → T → T ;
prod_one_left A: prod one A == A ;
prod_one_right A: prod A one == A ;
prod_assoc A B C: prod A (prod B C) == prod (prod A B) C ;
sum_zero_left A: sum zero A == A ;
sum_zero_right A: sum A zero == A ;
sum_assoc A B C: sum A (sum B C) == sum (sum A B) C ;
prod_zero_left A: prod zero A == zero ;
prod_zero_right A: prod A zero == zero ;
prod_sum_left A B C: prod (sum A B) C == sum (prod A C) (prod B C) ;
prod_sum_right A B C: prod C (sum A B) == sum (prod C A) (prod C B) ;
(* Fixme add distributivity *)
prod_Proper: Proper (equiv ==> equiv ==> equiv) prod ;
sum_Proper: Proper (equiv ==> equiv ==> equiv) sum ;
}.
Coercion T: Term >-> Sortclass.
Existing Instance Term_Setoid.
Existing Instance prod_Proper.
Existing Instance sum_Proper.
Notation "0" := zero.
Notation "1" := one.
Infix "*" := prod.
Infix "+" := sum.
End Term.
Module Import Hom.
Class Homomorphism {A B: Term} (map: A → B) := {
map_one: map 1 == 1 ;
map_zero: map 0 == 0 ;
map_prod x y: map (x * y) == map x * map y ;
map_sum x y: map (x + y) == map x + map y ;
map_Proper: Proper (equiv ==> equiv) map ;
}.
Existing Instance map_Proper.
Definition Hom (A B: Term) := { f: A → B | Homomorphism f}.
Definition Hom_Homomorphism {A B} (f: Hom A B): Homomorphism (proj1_sig f) := proj2_sig f.
Existing Instance Hom_Homomorphism.
#[program]
Definition id A: Hom A A := λ x, x.
Next Obligation.
Proof.
exists.
all: intros.
all: try reflexivity.
intros ? ? p.
auto.
Qed.
#[program]
Definition compose {A B C} (f: Hom B C) (g: Hom A B): Hom A C := λ x, f (g x).
Next Obligation.
Proof.
exists.
all: intros.
- repeat rewrite map_one.
reflexivity.
- repeat rewrite map_zero.
reflexivity.
- repeat rewrite map_prod.
reflexivity.
- repeat rewrite map_sum.
reflexivity.
- intros ? ? p.
rewrite p.
reflexivity.
Qed.
Infix "∘" := compose (at level 30).
End Hom.
(*
Instead of a free functor to the category of terms make some sort
of free bifunctor ?
I'm just not sure this quite makes sense.
*)
Module Free.
Inductive free {H: Type} {T: Term}: Type :=
| η (h: H) (t: T)
| one
| zero
| prod (A B: free)
| sum (A B: free)
.
Arguments free: clear implicits.
Inductive equiv {H T}: relation (free H T) :=
| reflexive: reflexive (free H T) equiv
| symmetric: symmetric (free H T) equiv
| transitive: transitive (free H T) equiv
| prod_one_left A: equiv (prod one A) A
| prod_one_right A: equiv (prod A one) A
| prod_assoc A B C: equiv (prod A (prod B C)) (prod (prod A B) C)
| sum_zero_left A: equiv (sum zero A) A
| sum_zero_right A: equiv (sum A zero) A
| sum_assoc A B C: equiv (sum A (sum B C)) (sum (sum A B) C)
| prod_zero_left A: equiv (prod zero A) zero
| prod_zero_right A: equiv (prod A zero) zero
| prod_sum_left A B C: equiv (prod (sum A B) C) (sum (prod A C) (prod B C))
| prod_sum_right A B C: equiv (prod C (sum A B)) (sum (prod C A) (prod C B))
| η_Proper h: Proper (SetoidClass.equiv ==> equiv) (η h)
| prod_Proper: Proper (equiv ==> equiv ==> equiv) prod
| sum_Proper: Proper (equiv ==> equiv ==> equiv) sum
.
Existing Instance η_Proper.
Existing Instance prod_Proper.
Existing Instance sum_Proper.
Instance free_Equivalence H T: Equivalence (@equiv H T) := {
Equivalence_Reflexive := reflexive ;
Equivalence_Symmetric := symmetric ;
Equivalence_Transitive := transitive ;
}.
Instance free_Setoid H T: Setoid (free H T) := {
equiv := equiv ;
}.
Instance free_Term H T: Term := {
T := free H T ;
one := one ;
zero := zero ;
prod := prod ;
sum := sum ;
prod_one_left := prod_one_left ;
prod_one_right := prod_one_right ;
prod_assoc := prod_assoc ;
sum_zero_left := sum_zero_left ;
sum_zero_right := sum_zero_right ;
sum_assoc := sum_assoc ;
prod_zero_left := prod_zero_left ;
prod_zero_right := prod_zero_right ;
prod_sum_left := prod_sum_left ;
prod_sum_right := prod_sum_right ;
prod_Proper := prod_Proper ;
sum_Proper := sum_Proper ;
}.
Infix "⊗" := free_Term (at level 60, right associativity).
Definition map_h {T A B} (op: A → B): free A T → free B T :=
fix loop p :=
match p with
| η x t => η (op x) t
| one => one
| zero => zero
| prod A B => prod (loop A) (loop B)
| sum A B => sum (loop A) (loop B)
end.
(* FIXME define Term homomorphism *)
Definition map_t {H} {A B: Term} (op: A → B): free H A → free H B :=
fix loop p :=
match p with
| η x t => η x (op t)
| one => one
| zero => zero
| prod A B => prod (loop A) (loop B)
| sum A B => sum (loop A) (loop B)
end.
(* FIXME seems wrong *)
Definition ε_h {A B: Term}: free A B → A :=
fix loop p :=
match p with
| η x _ => x
| one => 1
| zero => 0
| prod A B => loop A * loop B
| sum A B => loop A + loop B
end.
Definition ε_t {A} {B: Term}: free A B → B :=
fix loop p :=
match p with
| η _ y => y
| one => 1
| zero => 0
| prod A B => loop A * loop B
| sum A B => loop A + loop B
end.
(* FIXME seems wrong *)
Definition join {A B T}: A ⊗ (B ⊗ T) → B ⊗ T := ε_t.
#[program]
Fixpoint push {A B C} (p: (A * B) ⊗ C): A ⊗ (B ⊗ C) :=
match p with
| η ab t => η (fst ab) (η (snd ab) t)
| one => one
| zero => zero
| prod a b => prod (push a) (push b)
| sum a b => sum (push a) (push b)
end.
Instance push_Proper {A B C}: Proper (equiv ==> equiv) (@push A B C).
Proof.
intros ? ? p.
induction p.
all: cbn in *.
all: try reflexivity.
- symmetry.
auto.
- rewrite IHp1, IHp2.
reflexivity.
- rewrite prod_one_left.
reflexivity.
- rewrite prod_one_right.
reflexivity.
- rewrite prod_assoc.
reflexivity.
- rewrite sum_zero_left.
reflexivity.
- rewrite sum_zero_right.
reflexivity.
- rewrite sum_assoc.
reflexivity.
- rewrite prod_zero_left.
reflexivity.
- rewrite prod_zero_right.
reflexivity.
- rewrite prod_sum_left.
reflexivity.
- rewrite prod_sum_right.
reflexivity.
- rewrite H.
reflexivity.
- rewrite IHp1, IHp2.
reflexivity.
- rewrite IHp1, IHp2.
reflexivity.
Qed.
Instance push_Homomorphism {A B C}: Homomorphism (@push A B C).
Proof.
exists.
all: cbn.
- reflexivity.
- reflexivity.
- intros ? p.
reflexivity.
- intros ? p.
reflexivity.
- intros ? ? p.
rewrite p.
reflexivity.
Qed.
Definition pop {A B C} (p: A ⊗ (B ⊗ C)): (A * B) ⊗ C.
Admitted.
End Free.