15:34 <darchitect> hey guys, can someone please explain to me the difference between type theory and category theory as someone interested in abstract maths, but not necessarily formally educated in it (a programmer) wanting to delve deeper into type theory (using OCaml)

15:34 <darchitect> also any book recommendations would be welcome :)

15:38 <discocaml> <octachron> Category theory is a way to build abstraction for looking at abstract mathematics to make patterns emerge.

15:39 <discocaml> <octachron> Type theory for programming languages is more concerned at way to build abstraction/approximation for looking at programming languages to analyze their behavior (aka make pattern emerge).

15:40 <discocaml> <octachron> https://en.wikipedia.org/wiki/Types_and_Programming_Languages is well-known reference book.

15:41 <darchitect> discocaml: thanks ! I am going through Robert Harper's course on Programming Languages and there he mentions that a "sufficiently expressive programming language can be the basis of all mathematics". I guess that means that type theory is also used to build abstraction about maths similar to category theory (or am I missing something) ?

15:42 <discocaml> <octachron> With the main properties analyzed by type systems being "Does that program halt?", or "Does that program crash?" or "Does that program make sense"? aka "Is that program well-behaved?"

15:43 <discocaml> <octachron> The interpretation is more that one can use some programming language to write and prove mathematics. Which is what proof assistants (like Coq) are doing.

15:44 <darchitect> doesn't that mean we can express any form of mathematics using type thoery (some progrmaming language) meaning we can also express category theory in type theoretic terms ?

15:44 <darchitect> making type theory more or less the be-all-end-all ..

15:44 <darchitect> ?

15:46 <octachron> All mathematics can be expressed with set theory, being able to express all mathematics is not really a grand statement.

15:48 <darchitect> right..

15:49 <octachron> This is a similar situation with the parallel lambda calculus/Turing machine: both describes the same computable universe and both can be used to describe all programs.

15:49 <darchitect> so is category theory more "abstract/general" than type theory ? I guess what I am trying to wrap my head around is - what is highest level of abstraction I should begin my journey into "the new foundations" ?

15:49 <darchitect> from *

15:54 <octachron> I don't recommend for non-mathematicians to start with the highest level of abstraction available.

15:56 <octachron> You should start with the subject that interest you the most, and that you can connect with questions that you find interesting.

15:58 <octachron> (As a former mathematics-oriented physicist, I still find the idea of starting a mathematics journey with category theory headscratch-inducing).

16:03 <darchitect> can we express all the ideas expressable in Category Theory in Type theoretic terms ?

16:04 <darchitect> I am asking because it feels learning Type Theory first (from the point of someone wanting to learn more about programming langueage design) is more natural ?

16:11 <companion_cube> Type Theory is really nice and cool, whereas category theory will turn you into a raving fanatic that mumbles about diagrams all day

16:11 <companion_cube> (100% non subjective judgement here)

16:15 <octachron> Category theory and type theory mostly have a different subject (with some intersection).

16:16 <octachron> I would recommend to start with type theory if you want to be sure to learn at least a bit about programming language design.

16:17 <companion_cube> Church's simple theory ought to be enough for everyone™

16:17 <Fardale> companion_cube: *commutative* diagrams! Not all diagrams are equals ;-)

16:17 <companion_cube> see, there's the good diagrams and the bad diagrams

16:17 <companion_cube> the bad diagram, it has arrows, you see, they don't commute

16:18 <companion_cube> the good diagram, well, it has arrows, and they don't commute, but it's a good diagram

16:18 <darchitect> octachron: thank you! Also what do you think about starting with OCaml or Haskell first, I like Haskell's syntax, but I watched Robert Harper's lectures on PL design and he seems to be a pretty convinced opponent of it :d

16:21 <octachron> The importance of syntax is often overestimaged in my opinion. Both are a good choice. Personally, I prefer OCaml approach in general to build things first, and the specify them after.

16:22 <darchitect> as in -> not having function signatures ?

16:23 <octachron> ? Both OCaml and Haskell have `->` in function signatures?

16:24 <darchitect> no no I meant "as in - is 'not having to type function signatures' what makes you like OCaml's interface spec better" ?

16:25 <octachron> You also don't have to write down function signatures in Haskell.

16:25 <octachron> I am more talking about the general design of the languages.

16:26 <darchitect> are there any inherent reasons why one is better than the other for first getting into Type Theory ? (I personally like OCaml better for it's modules system and the better eco-system)

16:28 <octachron> The differences don't matter much if you are getting into Type theory.

16:29 <companion_cube> imho if you want to learn type theory and not just FP, just learn Coq or Lean

16:29 <companion_cube> OCaml and Haskell are really just programming languages

16:29 <discocaml> <._null._> If you prefer Haskell you can also go for Agda

16:30 <octachron> (that happens to have a type system that was though for humans)

17:05 <neiluj> hi! do objects have a deallocation method? like Python's __dealloc__?

17:07 <companion_cube> no, but you can use Gc.finalise

17:09 <neiluj> nice! thanks

20:19 <darchitect> hey guys, I want to start writing my first programming language using OCaml, can you please point to some good textbooks to start with ?

20:27 <discocaml> <deepspacejohn> I haven't used it personally, but the Cornell book has a section about writing an interpreter https://cs3110.github.io/textbook/chapters/interp/intro.html

20:35 <darchitect> discocaml: thank you !

20:35 <discocaml> <._null._> discocaml is the name of the bridge to Discord

20:36 <darchitect> btw I have watched this course and followed it through, I was hoping for something a bit more "intermediate" I guess, where I can apply the theory from Harper's PFPL to an actual machine with OCaml ?

21:50 <discocaml> <kakadu18> @darchitect I head Appel's 'Compiling with Continuations' is good, but kind of advanced..

21:50 <discocaml> <kakadu18> heard*