4 ms·

> The other thing that we do all the time in everyday life is a quotient, and as far as I know no programming language has a good way to represent that: somethi

> The other thing that we do all the time in everyday life is a quotient, and as far as I know no programming language has a good way to represent that: something as basic as a fraction How would the implementation of a general equivalence relation work? Just defining the equivalence relation does not yield a method for chosing a representative. Would you check the equivalence at each operation?

hiker 6y ago
If the focus is on finite data structures only and the equivalence relation is "are the types isomorphic", then each type is isomorphic to the ordinary generating functor with some coefficients C : N->N: -- ogf(c,x) = Σ n:ℕ, cₙ xⁿ def ogf (c : ℕ → ℕ) (α : Type) := Σ n:ℕ, fin (c n) × (fin n → α) (fin n is finite type with exactly n elements) For example list has coefficients Cn = {1,1,1,1...} inductive list (α : Type) | nil : list | cons (hd : α) (tl : list) : list and binary trees inductive bin_tree (α : Type) | leaf : bin_tree | branch (x : α) (left : bin_tree) (right : bin_tree) : bin_tree have coefficients the Catalan numbers {1,1,2,5,14,42,132,429,...}. Computing those coefficients from a type definition is not always trivial though (see the symbolic method http://algo.inria.fr/flajolet/Publications/AnaCombi/book.pdf http://algo.inria.fr/flajolet/Publications/AnaCombi/book.pdf). This can be extended to infinite data structures too by switching the natural numbers to ordinal numbers in the ogf definition.
zozbot234 6y ago
> Just defining the equivalence relation does not yield a method for chosing a representative. Would you check the equivalence at each operation? Choosing a canonical representative is not feasible in the general case, so yes one would need to prove that every operation respects the equivalence relation.
- choeger 6y ago
  What do you mean by "respects the equivalence relation"? Do you demand that f(x) ~ x implies that f(x) = x ? (~ being the equivalence and = being identity).
  - lmm 6y ago
    We demand that x ~ y implies f(x) ~ f(y).

hiker 6y ago

If the focus is on finite data structures only and the equivalence relation is "are the types isomorphic", then each type is isomorphic to the ordinary generating functor with some coefficients C : N->N: -- ogf(c,x) = Σ n:ℕ, cₙ xⁿ def ogf (c : ℕ → ℕ) (α : Type) := Σ n:ℕ, fin (c n) × (fin n → α) (fin n is finite type with exactly n elements) For example list has coefficients Cn = {1,1,1,1...} inductive list (α : Type) | nil : list | cons (hd : α) (tl : list) : list and binary trees inductive bin_tree (α : Type) | leaf : bin_tree | branch (x : α) (left : bin_tree) (right : bin_tree) : bin_tree have coefficients the Catalan numbers {1,1,2,5,14,42,132,429,...}. Computing those coefficients from a type definition is not always trivial though (see the symbolic method http://algo.inria.fr/flajolet/Publications/AnaCombi/book.pdf http://algo.inria.fr/flajolet/Publications/AnaCombi/book.pdf). This can be extended to infinite data structures too by switching the natural numbers to ordinal numbers in the ogf definition.

zozbot234 6y ago

> Just defining the equivalence relation does not yield a method for chosing a representative. Would you check the equivalence at each operation? Choosing a canonical representative is not feasible in the general case, so yes one would need to prove that every operation respects the equivalence relation.

choeger 6y ago
What do you mean by "respects the equivalence relation"? Do you demand that f(x) ~ x implies that f(x) = x ? (~ being the equivalence and = being identity).
- lmm 6y ago
  We demand that x ~ y implies f(x) ~ f(y).