Note: This channel on freenode is currently not being logged anymore. The logs are reproduced here for posterity.

2020-09-16 21:55:25 +0200 <geekosaur> where your type theory is the one chosen by the language designer, since most users won't be that interested in that particular level of detail
2020-09-16 21:55:35 +0200 <dolio> Algebraic types are already a schema for infinitely many acceptable definitions, though.
2020-09-16 21:55:41 +0200 <monochrom> I'll now refer you to two big volumes, "types and programming languages" and "practical foundations for programming languages". Pick one of them and study. I won't answer further questions until you have finished at least one. Your current questions and I bet the next 70 ones are all answered there.
2020-09-16 21:55:41 +0200 <Cale> But a good book recommendation might be "Types and Programming Languages" by Benjamin Pierce
2020-09-16 21:56:00 +0200cosimone(~cosimone@2001:b07:ae5:db26:b248:7aff:feea:34b6)
2020-09-16 21:56:59 +0200wroathe(~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2020-09-16 21:57:24 +0200gestone(~gestone@c-73-97-137-216.hsd1.wa.comcast.net) (Ping timeout: 260 seconds)
2020-09-16 21:58:50 +0200 <Cale> https://github.com/MPRI/M2-4-2/blob/master/Types%20and%20Programming%20Languages.pdf -- apparently it's just on github now
2020-09-16 21:59:01 +0200 <rustisafungus> yeah i was trying to find it :-P thanks
2020-09-16 21:59:05 +0200 <Cale> (this is probably not official)
2020-09-16 22:00:06 +0200jb55(~jb55@gateway/tor-sasl/jb55) (Remote host closed the connection)
2020-09-16 22:00:10 +0200machinedgod(~machinedg@d67-193-126-196.home3.cgocable.net)
2020-09-16 22:00:30 +0200jb55(~jb55@gateway/tor-sasl/jb55)
2020-09-16 22:01:52 +0200 <monochrom> Now I'm at a moral crossroad of "should I keep a copy?"
2020-09-16 22:02:38 +0200 <Cale> rustisafungus: There are programming languages like Coq and Agda whose types can encode all the statements of mathematics, and whose programs can literally be regarded as proofs of those statements, and where the fundamental building blocks of expressions correspond directly with logical rules.
2020-09-16 22:04:23 +0200supercoven(~Supercove@dsl-hkibng32-54fb54-166.dhcp.inet.fi) (Ping timeout: 272 seconds)
2020-09-16 22:04:28 +0200 <Cale> I own a paper copy, but it's nice to have the PDF :P
2020-09-16 22:04:37 +0200 <monochrom> Yeah that's fair.
2020-09-16 22:05:34 +0200 <Cale> Apparently it's just been sitting there for 5 years as well, and that repo is linked with Xavier Leroy's course... so maybe nobody has any issue with it
2020-09-16 22:06:26 +0200balbirs(~balbirs__@ozlabs.org)
2020-09-16 22:06:54 +0200stree(~stree@50-108-115-67.adr01.mskg.mi.frontiernet.net) (Remote host closed the connection)
2020-09-16 22:07:28 +0200hackagelti13 0.1.2.1 - Core functionality for LTI 1.3. https://hackage.haskell.org/package/lti13-0.1.2.1 (jade)
2020-09-16 22:08:17 +0200stree(~stree@50-108-115-67.adr01.mskg.mi.frontiernet.net)
2020-09-16 22:08:28 +0200hackageyesod-auth-lti13 0.1.2.1 - A yesod-auth plugin for LTI 1.3 https://hackage.haskell.org/package/yesod-auth-lti13-0.1.2.1 (jade)
2020-09-16 22:09:36 +0200geekosaur(42d52102@66.213.33.2) (Remote host closed the connection)
2020-09-16 22:10:39 +0200lc_(~lc@94.198.42.164)
2020-09-16 22:10:42 +0200 <lc_> bro
2020-09-16 22:10:46 +0200 <lc_> type classes are just interfaces
2020-09-16 22:11:10 +0200 <lc_> what's with the fancy name
2020-09-16 22:11:18 +0200 <Graypup_> i mean kinda but you can't get `this` in them afaik
2020-09-16 22:11:36 +0200 <monochrom> I agree. We don't need the fancy name "interface".
2020-09-16 22:11:49 +0200josh(~josh@c-67-164-104-206.hsd1.ca.comcast.net)
2020-09-16 22:12:15 +0200 <Graypup_> trying to get my hackage docs to build on their antique ghc863
2020-09-16 22:12:19 +0200 <monochrom> "interfaces" are just type classes.
2020-09-16 22:12:47 +0200juuandyy(~juuandyy@90.166.144.65)
2020-09-16 22:13:22 +0200 <lc_> I can't believe I didnt realize this before
2020-09-16 22:13:34 +0200gestone(~gestone@c-73-97-137-216.hsd1.wa.comcast.net)
2020-09-16 22:13:52 +0200juuandyy(~juuandyy@90.166.144.65) (Client Quit)
2020-09-16 22:14:06 +0200xff0x_(~fox@2001:1a81:52d0:6b00:59b8:5104:189c:a88e) (Ping timeout: 244 seconds)
2020-09-16 22:14:09 +0200 <sm[m]> aren't they also what some languages call "traits"
2020-09-16 22:14:13 +0200 <Graypup_> ........ where's ghc883 and other versions with working `text` package? https://i.imgur.com/Iz58tKy.png
2020-09-16 22:14:17 +0200 <Graypup_> the heck hackage
2020-09-16 22:14:46 +0200 <Graypup_> sm[m], a trait, at least in rust, is quite different from an interface because you can implement it on someone else's type
2020-09-16 22:15:10 +0200AlterEgo-(~ladew@124-198-158-163.dynamic.caiway.nl) (Quit: Leaving)
2020-09-16 22:15:14 +0200mariatsji(~mariatsji@2a01:79d:53aa:c66c:59f2:1ee3:fe3e:b848)
2020-09-16 22:15:30 +0200 <Graypup_> so you can put extensions on standard library types, containers, etc by making a trait and impl'ing it for them
2020-09-16 22:15:36 +0200xff0x_(~fox@2001:1a81:52d0:6b00:59b8:5104:189c:a88e)
2020-09-16 22:15:59 +0200 <rustisafungus> so i read the first chapter of pierce and barely glanced at the second and third
2020-09-16 22:16:18 +0200unlink__(~unlink2@p200300ebcf25bd0068eb9d9c94da2a17.dip0.t-ipconnect.de) (Remote host closed the connection)
2020-09-16 22:16:20 +0200 <dolio> That doesn't seem like the agreement.
2020-09-16 22:16:37 +0200unlink__(~unlink2@p200300ebcf25bd0068eb9d9c94da2a17.dip0.t-ipconnect.de)
2020-09-16 22:16:58 +0200 <rustisafungus> do i understand correctly that he is saying that a type system is essentially a usable *but inferior* way of proving properties of a program?
2020-09-16 22:18:02 +0200gestone(~gestone@c-73-97-137-216.hsd1.wa.comcast.net) (Ping timeout: 260 seconds)
2020-09-16 22:18:16 +0200 <hyperisco> lc_, good troll
2020-09-16 22:18:55 +0200thc202(~thc202@unaffiliated/thc202) (Ping timeout: 240 seconds)
2020-09-16 22:19:02 +0200 <lc_> literally not trolling
2020-09-16 22:19:07 +0200 <lc_> they're literally just interfaces
2020-09-16 22:19:19 +0200 <Graypup_> ..... what the heck hackage https://hackage.haskell.org/upload the script here doesn't find the docs for the /other/ package it *just* built
2020-09-16 22:19:47 +0200mariatsji(~mariatsji@2a01:79d:53aa:c66c:59f2:1ee3:fe3e:b848) (Ping timeout: 244 seconds)
2020-09-16 22:20:16 +0200 <sm[m]> Graypup_: isn't that something we can also do with haskell typeclasses
2020-09-16 22:20:27 +0200 <hyperisco> rustisafungus, don't know where you've got on this, but there are as many types as there are naturals, usually
2020-09-16 22:20:39 +0200 <Graypup_> sm[m], yes, but not with interfaces
2020-09-16 22:21:07 +0200 <Graypup_> also there's some higher kinded types stuff that traits in rust don't do
2020-09-16 22:21:19 +0200dead10cc(~dead10cc@2607:fea8:2c60:2d2:b401:59a1:1f1b:bfe)
2020-09-16 22:21:24 +0200 <Graypup_> you couldn't have a trait Monad I don't think but I don't know why
2020-09-16 22:21:28 +0200 <hyperisco> rustisafungus, which is why in some type theory papers the discussion just orients around Nat
2020-09-16 22:22:04 +0200 <tomsmeding> lc_: in Haskell, as a user of a library that defines a particular type T, you can define new class C and make T and instance of that class C
2020-09-16 22:22:09 +0200sm[m]persists in the belief that typeclass/interface/trait are more or less synonyms, then
2020-09-16 22:22:25 +0200 <rustisafungus> hyperisco: sounds nice at some fundamental level, but if i ingest code from github and apply some kind of rule which can identify "identical types" and then another rule which can identify "simple rearrangements/compositions/etc of previously encountered types" then i might see a slowing or tapering off of encountering of new types as i ingest more kilobytes of say, haskell
2020-09-16 22:22:31 +0200 <sm[m]> uh, except interface doesn't have implementation, my bad
2020-09-16 22:22:41 +0200 <tomsmeding> how would you do that in, e.g., Java/C++ or Go, which I think is the class of languages where "interface" means something
2020-09-16 22:22:46 +0200merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2020-09-16 22:22:55 +0200 <hyperisco> rustisafungus, at what level are you looking for an answer?
2020-09-16 22:23:17 +0200 <Graypup_> interface /can/ have implementation as of java 8 iirc
2020-09-16 22:23:25 +0200 <Graypup_> (default implementation)
2020-09-16 22:23:32 +0200 <rustisafungus> something a mortal amateur like me can understand
2020-09-16 22:23:37 +0200 <Graypup_> which allows for a gross misuse of them to produce multiple inheritance lololol
2020-09-16 22:23:38 +0200 <lc_> You define an interface with a certain set of internal methods. Then other library users define their own implemmentations of that interface by filling in the method descriptions
2020-09-16 22:23:43 +0200 <dolio> 'As many types as there are naturals' is kind of a dubious answer.
2020-09-16 22:23:54 +0200 <lc_> You dont need multiple inheritance or anything. Go has this. Every language has this
2020-09-16 22:24:01 +0200 <hyperisco> lc_, I can't count how many times this discussion has occurred on this channel. They're significantly not the same, assuming we're saying "interface" as in Java or something
2020-09-16 22:24:23 +0200 <Graypup_> interface is a distinctly OO thing for sure
2020-09-16 22:24:49 +0200 <lc_> https://golang.org/pkg/io/#Reader
2020-09-16 22:24:57 +0200 <lc_> ^ example of type class
2020-09-16 22:25:10 +0200 <hyperisco> there are few languages that have type classes
2020-09-16 22:25:23 +0200 <hyperisco> in fact I know of only 2, but there are likely more, and those would be Haskell and PureScript
2020-09-16 22:25:43 +0200 <tomsmeding> lc_: I'm not _terribly_ familiar with Go; suppose I define a new Go interface, say CoolReader, that requires a method CoolRead()
2020-09-16 22:25:55 +0200 <tomsmeding> and I want to implement that for some standard library type, say Stdin
2020-09-16 22:25:58 +0200 <tomsmeding> can I do that?
2020-09-16 22:26:05 +0200 <lc_> yes
2020-09-16 22:27:15 +0200 <tomsmeding> so to be clear, Go's interfaces are _not_ the same thing as C++/Java interfaces
2020-09-16 22:27:17 +0200 <hyperisco> or are you using my favourite approach where you just say something to provoke responses :P
2020-09-16 22:27:43 +0200 <lc_> All an interface is is a description of methods an object must support to be called "interface_name". So any struct you make which has those methods w/ those types, you can use and call "interface_name", and pass it into e.g. other outside libraries, etc.
2020-09-16 22:27:45 +0200 <ski> hyperisco : Clean,Mercury
2020-09-16 22:28:18 +0200merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds)
2020-09-16 22:28:24 +0200 <hyperisco> well now I know of 4
2020-09-16 22:28:38 +0200 <tomsmeding> lc_: a difference between Go interfaces and Haskell type classes is that in Go, a type automatically satisfies an interface if it has the required methods, whereas in Haskell you need to explicitly make the type a member
2020-09-16 22:28:39 +0200 <Graypup_> go interfaces are kinda like c++ concepts sorta: you don't have to say your type implements them, you implement them and then you have functions that can take things with that interface
2020-09-16 22:28:47 +0200 <Graypup_> lol we both said the same thing
2020-09-16 22:28:50 +0200 <tomsmeding> Graypup_: yup