July 8: Micah Halter et al.'s talk · event: ACT20

I think it's worth talking more about the similarity between Catlab and DisCoPy. People have Opinions about which language features are better than others and can argue in circles forever. Maybe it's a good idea to have multiple implementations of the same thing for that reason. But I worry about large scale duplicated effort between them

Mike Shulman (Jul 08 2020 at 17:14):

Is anyone implementing category theory in a statically typed language? I'm surprised that so many category theorists are using languages with dynamic types, which seem to me to be the opposite of the way category theory teaches us to think.

Jules Hedges (Jul 08 2020 at 17:15):

Eigil Rischel (Jul 08 2020 at 17:16):

Jules Hedges (Jul 08 2020 at 17:16):

Yes, open games are currently prototyped in Haskell, but I'm considering porting to Julia for various reasons

Toby Smithe (Jul 08 2020 at 17:16):

Jules Hedges (Jul 08 2020 at 17:17):

No, I don't think the question even really makes sense, but you can for sure fake it enough to work

Jules Hedges (Jul 08 2020 at 17:18):

In haskell, the typesystem statically prevents you from accessing the bound type in an invalid way. In any other language you can make it private and just trust the programmer not to do anything nasty

Toby Smithe (Jul 08 2020 at 17:18):

I'm with Mike. I wish Julia had dependent types! Otherwise, it's such a nice language. A proper type theory would make it perfect.

James Fairbanks (Jul 08 2020 at 17:18):

Hi Jules and Toby, let's talk more about open games in Catlab, I think we need to do more with optics in general.

Toby Smithe (Jul 08 2020 at 17:18):

Eigil Rischel (Jul 08 2020 at 17:20):

So here's a recurring question. My open games tool (https://github.com/jules-hedges/open-games-hs) is written for Haskell, but obviously I don't expect my target users to pick up Haskell. Ideally it would target something like Python. I have no idea how easy or hard that would be, but I'd guess hard

- julesh (@_julesh_)

Evan Patterson (Jul 08 2020 at 17:24):

As others have mentioned, doing CT in a statically typed language is the standard approach, and there is a long tradition of that in the Haskell community, for example. In principle, I'm not opposed at all to that approach, but where I come from (statistics and traditional applied math generally), the need to support scientific and numerical computation in a practical way is a paramount. Right now, Julia seems like the best compromise for a scientific computing language with reasonable programming language features.

Aleksandar Makelov (Jul 08 2020 at 17:26):

@Evan Patterson, what do you think are Python's main disadvantages compared to Julia?

Fabrizio Genovese (Jul 08 2020 at 17:26):

For us the most important thing is reliability instead. This is why we shoose to implement our libraries using formally verified languages. Idris is a good compromise here because it has dependent types, but it's really aimed at industry strength production

Evan Patterson (Jul 08 2020 at 17:28):

Right, if formal verification is your prime directive, then Julia is not going to help you much. So I think a lot depends on what you're trying to accomplish. There is definitely room for multiple approaches.

Fabrizio Genovese (Jul 08 2020 at 17:29):

Jules Hedges (Jul 08 2020 at 17:29):

Right, but Python and Julia seem very similar to each other. They are both dynamic and both used for heavy numerics

Evan Patterson (Jul 08 2020 at 17:30):

Right, there are two separate threads going on here, one about Julia vs static/dependently typed languages and one about Julia vs Python. Let me try to give my perspective on the second.

Mike Shulman (Jul 08 2020 at 17:47):

Is there some reason that "supporting scientific and numerical computation in a practical way" leads to the use of dynamic types? A priori they don't seem related to me; in fact it seems on a quick reading that part of what makes Julia performant is the ability of its compiler to optimize away the dynamic types!

Evan Patterson (Jul 08 2020 at 17:47):

As Jules says, both Python and Julia are commonly used for numerical computing. Python has going for it that it is easy to use and is popular in the (huge) ML community, so it has lots of mindshare. But Python suffers badly from what is sometimes called the "two language problem": it is too slow to directly support intensive computing, and so numerical code and data structures are written in languages like C, C++, and Fortran and wrapped for use in vectorized computing in Python. Julia was created to solve this problem, to have an easy-to-use language that is fast enough that your inner loops don't have to be written in C. Moreover, in ACT, a lot of the computing is also over discrete structures like graphs, for which farming out to other languages for speed becomes even more tedious.

Julia also has a number of language features, not possessed by Python, that are surprisingly well matched to ACT. One is its system for multiple type dispatch, so you can have a single generic function compose that works across any category. Good support for Unicode operators allows nice syntactic sugar for these functions, which matches the standard mathematical notation. Julia also has support for Lisp-style metaprogramming, which we use extensively. For example, the system for GATs (generalized algebraic theories) in Catlab effectively implements a simple form of dependent typing in Julia using metaprogramming.

Evan Patterson (Jul 08 2020 at 17:52):

I totally agree. There is no reason that this should necessarily lead to dynamic types and is in some ways opposed to it. Historically scientists and engineers have resisted types, but probably that's just because the classic languages with static types, like C, are really unpleasant.

Scientific computing currently seems to be converging not to dynamic typing but towards "gradual tying," where types are optional but recommended, in part because people have gradually realized that types are actually good for avoiding programming errors. Types in Julia are like this. In fact, if you look at the Catlab codebase, you'll see that basically every function is annotated with types, because we like to write in that style.

Mike Shulman (Jul 08 2020 at 17:54):

My understanding of "gradual typing" is that when the optional types are given, they should be static, i.e. checked at compile time. But my brief reading and experiments with Julia suggest that even when type annotations are given they are only checked at runtime. Is that correct?

James Fairbanks (Jul 08 2020 at 17:54):

I would second all of Evan's points. We find that multiple dispatch really lets you write code that looks like the math and we heavily exploit the lisp style macros to create DSLs embedded in Julia. Dynamic types are really popular in scientific computing because the users are scientists first and programmers seconds. You have to really think about types a lot in statically typed languages and in dynamic languages you can just write code without thinking about types too much. Julia gives you the best of both worlds because of gradual typing.

James Fairbanks (Jul 08 2020 at 17:55):

James Fairbanks (Jul 08 2020 at 17:56):

because it uses a just in time compiler, there is more than one compile time during the execution of the program. so yes the gradual types are static at compile time. There is just more than one compile time per execution

James Fairbanks (Jul 08 2020 at 17:58):

this is really important for us, because things like CSet{C} can be generated by runtime values of C.

Mike Shulman (Jul 08 2020 at 18:04):

Yes, everything I've seen about Julia seems pretty great except for the dynamicness of its typing. (Well, and maybe the 1-based array indexing.)

Evan Patterson (Jul 08 2020 at 18:04):

Mike Shulman (Jul 08 2020 at 18:05):

Maybe you're thinking of those people who call themselves mathematicians but don't admit 0 as a natural number?

Mike Shulman (Jul 08 2020 at 18:08):

I think I see what you mean about the JIT. But in practice it seems to me that this is less useful than true static typing. Consider the following example:

function foo(x::Int)
  x
end

function bar(y::String)
  foo(y)
end

It seems that this doesn't produce an error until bar is called. Maybe that's technically "compile time" because I guess the code isn't compiled until it's used, but it seems to me that it means that instead of being able to write my program, compile it, and be sure as soon as it compiles that I didn't make any type errors, I need to carefully write tests that cover all possible execution paths in order to be sure that "all the code is compiled" and therefore typechecked. That doesn't feel like static typing to me.

Mike Shulman (Jul 08 2020 at 18:09):

Ok let's take the flame war about natural numbers elsewhere, it is definitely off-topic here. (-:O

Mike Shulman (Jul 08 2020 at 18:09):

James Fairbanks (Jul 08 2020 at 18:11):

yeah, it definitely is a compromise relative to statically typed language for your purposes. But in scientific computing if you want to run at the largest scales aka "the petaflop club", your options are C/C++, Fortran, and Julia https://juliacomputing.com/case-studies/celeste.html

Aleksandar Makelov (Jul 08 2020 at 18:12):

is there currently a Julia library comparable to pytorch/tensorflow/etc in capability?

James Fairbanks (Jul 08 2020 at 18:15):

Given the huge amount of money Google has spent on TF, there is not an equally powerful library in Julia. You can use TF from Julia with Tensorflow.jl which links against the standard TF tools, and you can use a pure julia implementation DNNs with Flux.jl which is better for doing DNN research because it is pure julia with no dependence on black box C++ libs.

James Fairbanks (Jul 08 2020 at 18:17):

Maybe at ACT 2021 we will have a Catlab implementation of ParaParaEuc or @Toby Smithe's optics of learning framework

Mike Shulman (Jul 08 2020 at 18:17):

Given that Julia does know how to compile and to check types when it compiles, couldn't there be some flag one could pass to it instructing it to compile (and hence typecheck) everything rather than waiting for JIT? (I suppose probably this wouldn't catch everything since with parametrized types etc. there might always be some code that has to be compiled JIT, but it would be better than nothing.)

James Fairbanks (Jul 08 2020 at 18:17):

Toby Smithe (Jul 08 2020 at 18:17):

James Fairbanks (Jul 08 2020 at 18:18):

Toby Smithe (Jul 08 2020 at 18:19):

Yes, but right now I'm due to have supper..! (It's evening in Oxford now) Let's arrange something :-)

Evan Patterson (Jul 08 2020 at 18:20):

Yes, it's a practical problem for certain kinds of deployments. Work in progress on this is happening at PackageCompiler.jl.

Micah Halter (Jul 08 2020 at 20:39):

Building off what @James Fairbanks presented in our talk this afternoon, I am going to drop some links here of working examples using Catlab and other AlgebraicJulia packages as a way to rapidly develop different types of models specifically on using open petri nets and decorated cospans. AlgebraicPetri.jl is the package that connects Catlab as a categorical interface for the Petri net simulation library in Julia Petri.jl. A few basic examples can be found in the AlgebraicPetri.jl documentation:

Stream: event: ACT20

Topic: July 8: Micah Halter et al.'s talk

Paolo Perrone (Jul 02 2020 at 02:08):

Paolo Perrone (Jul 08 2020 at 15:56):

Jules Hedges (Jul 08 2020 at 17:01):

Mike Shulman (Jul 08 2020 at 17:14):

Jules Hedges (Jul 08 2020 at 17:15):

Eigil Rischel (Jul 08 2020 at 17:16):

Jules Hedges (Jul 08 2020 at 17:16):

Toby Smithe (Jul 08 2020 at 17:16):

Jules Hedges (Jul 08 2020 at 17:17):

Jules Hedges (Jul 08 2020 at 17:18):

Toby Smithe (Jul 08 2020 at 17:18):

James Fairbanks (Jul 08 2020 at 17:18):

Toby Smithe (Jul 08 2020 at 17:18):

Eigil Rischel (Jul 08 2020 at 17:20):

Evan Patterson (Jul 08 2020 at 17:24):

Aleksandar Makelov (Jul 08 2020 at 17:26):

Fabrizio Genovese (Jul 08 2020 at 17:26):

Evan Patterson (Jul 08 2020 at 17:28):

Fabrizio Genovese (Jul 08 2020 at 17:29):

Jules Hedges (Jul 08 2020 at 17:29):

Evan Patterson (Jul 08 2020 at 17:30):

Mike Shulman (Jul 08 2020 at 17:47):

Evan Patterson (Jul 08 2020 at 17:47):

Evan Patterson (Jul 08 2020 at 17:52):

Mike Shulman (Jul 08 2020 at 17:54):

James Fairbanks (Jul 08 2020 at 17:54):

James Fairbanks (Jul 08 2020 at 17:55):

James Fairbanks (Jul 08 2020 at 17:56):

James Fairbanks (Jul 08 2020 at 17:58):

Mike Shulman (Jul 08 2020 at 18:04):

Evan Patterson (Jul 08 2020 at 18:04):

Mike Shulman (Jul 08 2020 at 18:05):

Mike Shulman (Jul 08 2020 at 18:08):

Mike Shulman (Jul 08 2020 at 18:09):

Mike Shulman (Jul 08 2020 at 18:09):

James Fairbanks (Jul 08 2020 at 18:11):

Aleksandar Makelov (Jul 08 2020 at 18:12):

James Fairbanks (Jul 08 2020 at 18:15):

James Fairbanks (Jul 08 2020 at 18:17):

Mike Shulman (Jul 08 2020 at 18:17):

James Fairbanks (Jul 08 2020 at 18:17):

Toby Smithe (Jul 08 2020 at 18:17):

James Fairbanks (Jul 08 2020 at 18:18):

James Fairbanks (Jul 08 2020 at 18:18):

Toby Smithe (Jul 08 2020 at 18:19):

Evan Patterson (Jul 08 2020 at 18:20):

Micah Halter (Jul 08 2020 at 20:39):

Paolo Perrone (Jul 08 2020 at 23:14):