3 ms·

> Dependency is pervasive throughout mathematics. What is a monoid? It’s a set M, and then operations m,e on M, and then conditions on m,e. Most objects are con

> Dependency is pervasive throughout mathematics. What is a monoid? It’s a set M, and then operations m,e on M, and then conditions on m,e. Most objects are constructed in layers, each of which depends on the ones before. Type theory is often regarded as “fancy” and only necessary in complex situations, similar to misperceptions of category theory; yet dependent types are everywhere. A monoid is (S,•,e): a set S equipped with a binary operation • : (S,S) -> S such that for all x, y, z in S, x•(y•z)=(x•y)•z, and an element e in S such that for all x in S, x•e=e•x=x. Examples of monoids include (String,concat,""), (int,0,+) and so on. One recurring theme in universal algebra and category theory is the notion of an algebra[0], in programmer terms it's like a module declaration. (see also F-algebra[1] which is heavily used in functional programming to formalize the notion of folding and more) Dependent type theory allows one to encode these algebras, e.g. encoding monoids and their laws in Coq's type system CoC[2]. Just like how ADTs in Haskell/OCaml and enums in Rust are comprised of a "sum of products", products and sums can be generalized in dependent types as well: Length-indexed lists via the dependent sum: Σn:ℕ.List(n) consists of dependent pairs ⟨n,l:List(n)⟩. Σn:ℕ.List(n) can be read as a function that takes a natural number n and returns a type List(n) Type-parametrized types: ΠS:Set.List(S) consists of dependent functions λS:Set.φ(S), ΠS:Set.List(S) can be read as a function that takes a type S and returns a type List(S) So to encode monoids in a dependent type theory using those dependent sums and products, we can just put the operations and laws into some big record, say Monoid:= ΣM:Set. Σm:M²→M. Σe:()→M. Π(a,b,c):M³.m(m(a,b),c)=m(a,m(b,c)). Πa:M.m(e,a)=a=m(a,e). Compare this to [2]! [0] https://en.wikipedia.org/wiki/Universal_algebra#Basic_idea https://en.wikipedia.org/wiki/Universal_algebra#Basic_idea [1] https://en.wikipedia.org/wiki/F-algebra https://en.wikipedia.org/wiki/F-algebra [2] https://gist.github.com/puffnfresh/11258181#file-monoid-v-L5 https://gist.github.com/puffnfresh/11258181#file-monoid-v-L5

siraben 6y ago
> For now we explore the language of a topos. There are multiple views, and often its full power is not used. Toposes support geometric logic, predicate logic, and moreover dependent type theory. We emphasize the latter: dependent types are expressive and pervasive, yet underutilized in mathematics. The next step of the article is the realization that a topos[0] has this expressive capability from the get-go. There's a nice list of clarifying examples in the paper[1], starting at the bottom of page 2, for instance, stacks with push and pop, untyped lambda calculus, monad comprehension syntax in Haskell (sort of like a generalization of async/await syntax), and so on. This quote in particular seems exciting: We aim to implement native type theory as a tool which inputs the formal semantics of a language and outputs a type system, which can then be used to condition an entire codebase. Properly integrated, it could introduce expressive type theory directly into everyday programming. To do so, we plan to utilize the progress made in language specification [0] https://en.wikipedia.org/wiki/Topos https://en.wikipedia.org/wiki/Topos [1] https://arxiv.org/pdf/2102.04672.pdf https://arxiv.org/pdf/2102.04672.pdf
creata 6y ago
But don't most dependent type theories have a restrictive notion of equality (e.g. without extensional equality of functions) making many things that we would like to be monoids not fit that definition? Anyway, I agree with your general point: dependent types are extremely simple, and make so many things more elegant (type-safe printf is the common example) that I'm surprised they aren't more popular.
- siraben 6y ago
  Hm yes. For instance the monoid of endofunctions on S would require one to prove that f . id = id . f = f. In vanilla dependent types this needs the extensionality axiom added, but in category theory it definitely is fine to speak of equality between morphisms with the same source and target.

siraben 6y ago

> For now we explore the language of a topos. There are multiple views, and often its full power is not used. Toposes support geometric logic, predicate logic, and moreover dependent type theory. We emphasize the latter: dependent types are expressive and pervasive, yet underutilized in mathematics. The next step of the article is the realization that a topos[0] has this expressive capability from the get-go. There's a nice list of clarifying examples in the paper[1], starting at the bottom of page 2, for instance, stacks with push and pop, untyped lambda calculus, monad comprehension syntax in Haskell (sort of like a generalization of async/await syntax), and so on. This quote in particular seems exciting: We aim to implement native type theory as a tool which inputs the formal semantics of a language and outputs a type system, which can then be used to condition an entire codebase. Properly integrated, it could introduce expressive type theory directly into everyday programming. To do so, we plan to utilize the progress made in language specification [0] https://en.wikipedia.org/wiki/Topos https://en.wikipedia.org/wiki/Topos [1] https://arxiv.org/pdf/2102.04672.pdf https://arxiv.org/pdf/2102.04672.pdf

creata 6y ago

But don't most dependent type theories have a restrictive notion of equality (e.g. without extensional equality of functions) making many things that we would like to be monoids not fit that definition? Anyway, I agree with your general point: dependent types are extremely simple, and make so many things more elegant (type-safe printf is the common example) that I'm surprised they aren't more popular.

siraben 6y ago
Hm yes. For instance the monoid of endofunctions on S would require one to prove that f . id = id . f = f. In vanilla dependent types this needs the extensionality axiom added, but in category theory it definitely is fine to speak of equality between morphisms with the same source and target.