4 ms·

I followed this until the part just slightly after "see how natural it is?" Then it's suddenly How to Draw an Owl. I don't follow the monoid part. Anyone can he

by chewxy 6y ago

I followed this until the part just slightly after "see how natural it is?" Then it's suddenly How to Draw an Owl. I don't follow the monoid part. Anyone can help elaborate?

siraben 6y ago
> 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.
lmm 6y ago
That's just an example of how we naturally use dependent types in everyday mathematics: the set of monoids is the set of triplets of a set M, a function m from that M^2 to that M, and an element 1 of that set M such that the given laws hold. You can only define the type of monoids (members of the set of monoids) dependently, because 1 isn't just an element of any set, it's an element of the specific set M. (Groups might have been a better example than monoids, given that groups are more familiar to mathematicians and the point is to emphasise that this is normal everyday mathematics).
- tomp 6y ago
  Not really, Rossberg’s 1ML / F-ing modules provides a way to elaborate such type to plain System F types, i.e. existentials, but not dependent types. The type of such monoid would be: exists[T] . (M : [= T], f : T -> T, e : T)
  - lmm 6y ago
    Sure, but that's distinctly not the way you'd write or think about that definition in everyday mathematics. It encodes the definition but it doesn't really express it.
  - GregarianChild 6y ago
    I think you need HKTs, in other words System F-omega, to carry out Rossberg's idea.
    - tomp 6y ago
      Only for applicative functors (i.e. OCaml’s version, where Set[int].t == Set[int].t), which 1ML models as pure functions.
tom_mellior 6y ago
The core sentence of the post comes a bit later, just above the "Conclusion" section header: "This type theory is used in proof assistants such as Coq and Agda; eventually, this expressive logic + dependent types will be utilized in many programming languages." Note the "is used" part, which is in the present tense. My understanding is that nothing new was constructed here. Maybe the well-known theory of dependent types has been reconstructed in a new way based on categories; this may be exciting to fans of category theory, but I don't see how it advances programming languages in any way. The actual paper isn't any more helpful either: It name-drops JavaScript in the introduction and at the very end, but doesn't really do anything with it, it certainly doesn't show any kind of model of a type system for even a trivial JavaScript subset.

by chewxy 6y ago

I followed this until the part just slightly after "see how natural it is?" Then it's suddenly How to Draw an Owl. I don't follow the monoid part. Anyone can help elaborate?

siraben 6y ago

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

lmm 6y ago

That's just an example of how we naturally use dependent types in everyday mathematics: the set of monoids is the set of triplets of a set M, a function m from that M^2 to that M, and an element 1 of that set M such that the given laws hold. You can only define the type of monoids (members of the set of monoids) dependently, because 1 isn't just an element of any set, it's an element of the specific set M. (Groups might have been a better example than monoids, given that groups are more familiar to mathematicians and the point is to emphasise that this is normal everyday mathematics).

tomp 6y ago
Not really, Rossberg’s 1ML / F-ing modules provides a way to elaborate such type to plain System F types, i.e. existentials, but not dependent types. The type of such monoid would be: exists[T] . (M : [= T], f : T -> T, e : T)
- lmm 6y ago
  Sure, but that's distinctly not the way you'd write or think about that definition in everyday mathematics. It encodes the definition but it doesn't really express it.
- GregarianChild 6y ago
  I think you need HKTs, in other words System F-omega, to carry out Rossberg's idea.
  - tomp 6y ago
    Only for applicative functors (i.e. OCaml’s version, where Set[int].t == Set[int].t), which 1ML models as pure functions.

tom_mellior 6y ago

The core sentence of the post comes a bit later, just above the "Conclusion" section header: "This type theory is used in proof assistants such as Coq and Agda; eventually, this expressive logic + dependent types will be utilized in many programming languages." Note the "is used" part, which is in the present tense. My understanding is that nothing new was constructed here. Maybe the well-known theory of dependent types has been reconstructed in a new way based on categories; this may be exciting to fans of category theory, but I don't see how it advances programming languages in any way. The actual paper isn't any more helpful either: It name-drops JavaScript in the introduction and at the very end, but doesn't really do anything with it, it certainly doesn't show any kind of model of a type system for even a trivial JavaScript subset.