You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Daniel Geisler (May 19 2020 at 09:24):Are julia and python the programming languages we want to use for scientific programming?
Pastel Raschke (May 19 2020 at 10:51):who's we?
julia seems to be a language a lot of people want to use for scientific programming, and its multiple dispatch model and type system feels very elegant to me on a PL level
this doesn't particularly strike me as applied ct
James Fairbanks (May 19 2020 at 12:04):Julia makes a lot of sense because of the type system. Having parametric and dependent types is useful for CT and being dynamically typed and fast is good for applications in scientific computing.
Dan Doel (May 19 2020 at 16:31):Julia doesn't appear to really have dependent types in the sense that most type theories useful for mathematics have them.
You need to be careful, because some people will describe a programming language as "having dependent types" when it just means that you can have types parameterized by static integer numerals, say, because statically sized vectors are a common simple example of dependent types. However, this does not mean that types can depend on values of arbitrary other types, or that there are things like Π, Σ and identity types that allow you to write proofs about the behavior of operations and such.
Philip Zucker (May 19 2020 at 19:55):There's an interesting, but al little too hot blooded discussion of the same here https://github.com/JuliaLang/julia/issues/6113
Philip Zucker (May 19 2020 at 19:57):Interestingly, firing up the repl, it appears you can parametrize types over more values than just ints. It accepts Tuple{1.34, 'a'} as a type for example.
Reid Barton (May 19 2020 at 20:02):I don't know Julia. Is that supposed to be the type of a pair whose first element is a 1.34 and whose second element is a 'a'?
Philip Zucker (May 19 2020 at 20:06):I think it is the analog of a pair whose first type slot is 1.34 and second type slot is 'a'
Philip Zucker (May 19 2020 at 20:06):I assume such a type can't be inhabitted
Reid Barton (May 19 2020 at 20:06):So even their types are untyped :upside_down:
Philip Zucker (May 19 2020 at 20:06):It is odd
Philip Zucker (May 19 2020 at 20:08):I would guess this capability is rarely used except for typelevel ints, but I'd be interested to see a place where it is
Philip Zucker (May 19 2020 at 20:12):To the original question, yes, python and julia are the leading candidates for a different flavor of category theory than you'll find in proof systems and ML-like languages.
Philip Zucker (May 19 2020 at 20:12):To my taste at least
Philip Zucker (May 19 2020 at 20:13):Category theory is used as a mathematical object to prove things about or used as a method for organizing proofs of other fields in those systems. The end result produced by the computer is mostly "typechecked" or "failed to typecheck".
Philip Zucker (May 19 2020 at 20:15):But there are different kinds of things one wants to do with a computer. Sometimes computers are useful for calculating something, something numerical in particular. And it seems like category theory can be useful for organizing those computations too
Philip Zucker (May 19 2020 at 20:17):Ideally, systems like Agda and Coq would be so easy to use and fast that one could do heavy duty numerical calculation in them with proof assurance backing the calculations. But the world isn't there yet, and figuring out how to even do simple numerical problems in those systems is still at the edge of my capabilities, despite not being an idiot and trying for a long time.
Philip Zucker (May 19 2020 at 20:20):So it seems like python and julia are the way to go at the moment if your aims are calculation. I actually find it freeing and mind expanding to not even have the _option_ of being a hard ass formalist, because such an approach is rather silly in a system not built for it.
Philip Zucker (May 19 2020 at 20:20):Also, if you're interested in having wider appeal, the barrier the entry of python and julia is much lower.
Fabrizio Genovese (May 19 2020 at 20:46):Daniel Geisler said:
Are julia and python the programming languages we want to use for scientific programming?
It depends what you want to do. For sure I wouldn't ever use either for theorem proving, for instance. Python is more or less the standard in AI tho.
Fabrizio Genovese (May 19 2020 at 20:48):Reid Barton said:
So even their types are untyped :upside_down:
This is not surprising tho. There's plenty of examples of "typed languages" whose types are a mess. Javascript comes to mind, really
Fabrizio Genovese (May 19 2020 at 20:48):All in all, for me a language is typed if you can clearly point me to a formal type theory that the language implements. Otherwise it's not typed, at best "hacked".
Nathanael Arkor (May 19 2020 at 20:52):All in all, for me a language is typed if you can clearly point me to a formal type theory that the language implements.
This criterion excludes almost all existing programming languages, including those for proof assistants, so this is a little stricter than common convention.
Fabrizio Genovese (May 19 2020 at 20:55):Lol, well yes
Fabrizio Genovese (May 19 2020 at 20:55):But c'mon, coming from category theory don't you feel an intrinsic sense of disgust in saying that C is typed? :D
Fabrizio Genovese (May 19 2020 at 20:56):Probably what I said makes more sense if you see things from a functional programming PoV, actually :slight_smile: