Logs: freenode/#haskell
| 2020-09-16 19:55:25 | <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 19:55:35 | <dolio> | Algebraic types are already a schema for infinitely many acceptable definitions, though. |
| 2020-09-16 19:55:41 | <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 19:55:41 | <Cale> | But a good book recommendation might be "Types and Programming Languages" by Benjamin Pierce |
| 2020-09-16 19:56:00 | → | cosimone joins (~cosimone@2001:b07:ae5:db26:b248:7aff:feea:34b6) |
| 2020-09-16 19:56:59 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2020-09-16 19:57:24 | × | gestone quits (~gestone@c-73-97-137-216.hsd1.wa.comcast.net) (Ping timeout: 260 seconds) |
| 2020-09-16 19:58:50 | <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 19:59:01 | <rustisafungus> | yeah i was trying to find it :-P thanks |
| 2020-09-16 19:59:05 | <Cale> | (this is probably not official) |
| 2020-09-16 20:00:06 | × | jb55 quits (~jb55@gateway/tor-sasl/jb55) (Remote host closed the connection) |
| 2020-09-16 20:00:10 | → | machinedgod joins (~machinedg@d67-193-126-196.home3.cgocable.net) |
| 2020-09-16 20:00:30 | → | jb55 joins (~jb55@gateway/tor-sasl/jb55) |
| 2020-09-16 20:01:52 | <monochrom> | Now I'm at a moral crossroad of "should I keep a copy?" |
| 2020-09-16 20:02:38 | <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 20:04:23 | × | supercoven quits (~Supercove@dsl-hkibng32-54fb54-166.dhcp.inet.fi) (Ping timeout: 272 seconds) |
| 2020-09-16 20:04:28 | <Cale> | I own a paper copy, but it's nice to have the PDF :P |
| 2020-09-16 20:04:37 | <monochrom> | Yeah that's fair. |
| 2020-09-16 20:05:34 | <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 20:06:26 | → | balbirs joins (~balbirs__@ozlabs.org) |
| 2020-09-16 20:06:54 | × | stree quits (~stree@50-108-115-67.adr01.mskg.mi.frontiernet.net) (Remote host closed the connection) |
| 2020-09-16 20:07:28 | hackage | lti13 0.1.2.1 - Core functionality for LTI 1.3. https://hackage.haskell.org/package/lti13-0.1.2.1 (jade) |
| 2020-09-16 20:08:17 | → | stree joins (~stree@50-108-115-67.adr01.mskg.mi.frontiernet.net) |
| 2020-09-16 20:08:28 | hackage | yesod-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 20:09:36 | × | geekosaur quits (42d52102@66.213.33.2) (Remote host closed the connection) |
| 2020-09-16 20:10:39 | → | lc_ joins (~lc@94.198.42.164) |
| 2020-09-16 20:10:42 | <lc_> | bro |
| 2020-09-16 20:10:46 | <lc_> | type classes are just interfaces |
| 2020-09-16 20:11:10 | <lc_> | what's with the fancy name |
| 2020-09-16 20:11:18 | <Graypup_> | i mean kinda but you can't get `this` in them afaik |
| 2020-09-16 20:11:36 | <monochrom> | I agree. We don't need the fancy name "interface". |
| 2020-09-16 20:11:49 | → | josh joins (~josh@c-67-164-104-206.hsd1.ca.comcast.net) |
| 2020-09-16 20:12:15 | <Graypup_> | trying to get my hackage docs to build on their antique ghc863 |
| 2020-09-16 20:12:19 | <monochrom> | "interfaces" are just type classes. |
| 2020-09-16 20:12:47 | → | juuandyy joins (~juuandyy@90.166.144.65) |
| 2020-09-16 20:13:22 | <lc_> | I can't believe I didnt realize this before |
| 2020-09-16 20:13:34 | → | gestone joins (~gestone@c-73-97-137-216.hsd1.wa.comcast.net) |
| 2020-09-16 20:13:52 | × | juuandyy quits (~juuandyy@90.166.144.65) (Client Quit) |
| 2020-09-16 20:14:06 | × | xff0x_ quits (~fox@2001:1a81:52d0:6b00:59b8:5104:189c:a88e) (Ping timeout: 244 seconds) |
| 2020-09-16 20:14:09 | <sm[m]> | aren't they also what some languages call "traits" |
| 2020-09-16 20:14:13 | <Graypup_> | ........ where's ghc883 and other versions with working `text` package? https://i.imgur.com/Iz58tKy.png |
| 2020-09-16 20:14:17 | <Graypup_> | the heck hackage |
| 2020-09-16 20:14:46 | <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 20:15:10 | × | AlterEgo- quits (~ladew@124-198-158-163.dynamic.caiway.nl) (Quit: Leaving) |
| 2020-09-16 20:15:14 | → | mariatsji joins (~mariatsji@2a01:79d:53aa:c66c:59f2:1ee3:fe3e:b848) |
| 2020-09-16 20:15:30 | <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 20:15:36 | → | xff0x_ joins (~fox@2001:1a81:52d0:6b00:59b8:5104:189c:a88e) |
| 2020-09-16 20:15:59 | <rustisafungus> | so i read the first chapter of pierce and barely glanced at the second and third |
| 2020-09-16 20:16:18 | × | unlink__ quits (~unlink2@p200300ebcf25bd0068eb9d9c94da2a17.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 2020-09-16 20:16:20 | <dolio> | That doesn't seem like the agreement. |
| 2020-09-16 20:16:37 | → | unlink__ joins (~unlink2@p200300ebcf25bd0068eb9d9c94da2a17.dip0.t-ipconnect.de) |
| 2020-09-16 20:16:58 | <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 20:18:02 | × | gestone quits (~gestone@c-73-97-137-216.hsd1.wa.comcast.net) (Ping timeout: 260 seconds) |
| 2020-09-16 20:18:16 | <hyperisco> | lc_, good troll |
| 2020-09-16 20:18:55 | × | thc202 quits (~thc202@unaffiliated/thc202) (Ping timeout: 240 seconds) |
| 2020-09-16 20:19:02 | <lc_> | literally not trolling |
| 2020-09-16 20:19:07 | <lc_> | they're literally just interfaces |
| 2020-09-16 20:19:19 | <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 20:19:47 | × | mariatsji quits (~mariatsji@2a01:79d:53aa:c66c:59f2:1ee3:fe3e:b848) (Ping timeout: 244 seconds) |
| 2020-09-16 20:20:16 | <sm[m]> | Graypup_: isn't that something we can also do with haskell typeclasses |
| 2020-09-16 20:20:27 | <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 20:20:39 | <Graypup_> | sm[m], yes, but not with interfaces |
| 2020-09-16 20:21:07 | <Graypup_> | also there's some higher kinded types stuff that traits in rust don't do |
| 2020-09-16 20:21:19 | → | dead10cc joins (~dead10cc@2607:fea8:2c60:2d2:b401:59a1:1f1b:bfe) |
| 2020-09-16 20:21:24 | <Graypup_> | you couldn't have a trait Monad I don't think but I don't know why |
| 2020-09-16 20:21:28 | <hyperisco> | rustisafungus, which is why in some type theory papers the discussion just orients around Nat |
| 2020-09-16 20:22:04 | <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 20:22:09 | sm[m] | persists in the belief that typeclass/interface/trait are more or less synonyms, then |
| 2020-09-16 20:22:25 | <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 20:22:31 | <sm[m]> | uh, except interface doesn't have implementation, my bad |
| 2020-09-16 20:22:41 | <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 20:22:46 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2020-09-16 20:22:55 | <hyperisco> | rustisafungus, at what level are you looking for an answer? |
| 2020-09-16 20:23:17 | <Graypup_> | interface /can/ have implementation as of java 8 iirc |
| 2020-09-16 20:23:25 | <Graypup_> | (default implementation) |
| 2020-09-16 20:23:32 | <rustisafungus> | something a mortal amateur like me can understand |
| 2020-09-16 20:23:37 | <Graypup_> | which allows for a gross misuse of them to produce multiple inheritance lololol |
| 2020-09-16 20:23:38 | <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 20:23:43 | <dolio> | 'As many types as there are naturals' is kind of a dubious answer. |
| 2020-09-16 20:23:54 | <lc_> | You dont need multiple inheritance or anything. Go has this. Every language has this |
| 2020-09-16 20:24:01 | <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 20:24:23 | <Graypup_> | interface is a distinctly OO thing for sure |
| 2020-09-16 20:24:49 | <lc_> | https://golang.org/pkg/io/#Reader |
| 2020-09-16 20:24:57 | <lc_> | ^ example of type class |
| 2020-09-16 20:25:10 | <hyperisco> | there are few languages that have type classes |
| 2020-09-16 20:25:23 | <hyperisco> | in fact I know of only 2, but there are likely more, and those would be Haskell and PureScript |
| 2020-09-16 20:25:43 | <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 20:25:55 | <tomsmeding> | and I want to implement that for some standard library type, say Stdin |
| 2020-09-16 20:25:58 | <tomsmeding> | can I do that? |
| 2020-09-16 20:26:05 | <lc_> | yes |
| 2020-09-16 20:27:15 | <tomsmeding> | so to be clear, Go's interfaces are _not_ the same thing as C++/Java interfaces |
| 2020-09-16 20:27:17 | <hyperisco> | or are you using my favourite approach where you just say something to provoke responses :P |
| 2020-09-16 20:27:43 | <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 20:27:45 | <ski> | hyperisco : Clean,Mercury |
| 2020-09-16 20:28:18 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 2020-09-16 20:28:24 | <hyperisco> | well now I know of 4 |
| 2020-09-16 20:28:38 | <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 20:28:39 | <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 20:28:47 | <Graypup_> | lol we both said the same thing |
| 2020-09-16 20:28:50 | <tomsmeding> | Graypup_: yup |
All times are in UTC.