WEBVTT 00:00:07.370 --> 00:00:09.500 >> hello and welcome to the Haskell weekly podcast. 00:00:09.680 --> 00:00:13.130 This is a show about Haskell a purely functional programming language. 00:00:13.370 --> 00:00:16.930 I'm your host, Cameron Gera, an engineer here at ITProTV. 00:00:17.180 --> 00:00:19.130 And with me today is Taylor Fausak. 00:00:19.370 --> 00:00:22.010 One of the engineers on my team and my boss. 00:00:22.400 --> 00:00:23.660 Thanks for joining me today, Taylor. 00:00:24.410 --> 00:00:27.200 >> Yeah, I'm happy to be here, cam, and I'm really excited 00:00:27.200 --> 00:00:31.500 today because we have a special guest with us, Sandy McGuire. 00:00:31.590 --> 00:00:32.670 Thanks for joining us, Sandy. 00:00:33.030 --> 00:00:34.170 >> Thanks for having me guys. 00:00:34.170 --> 00:00:35.160 I'm excited to be here. 00:00:35.520 --> 00:00:36.630 >> Yeah, this is awesome. 00:00:36.750 --> 00:00:40.830 So Sandy, for people who may not know who you are already, 00:00:41.190 --> 00:00:42.360 how would you describe yourself? 00:00:43.500 --> 00:00:45.420 >> Uh, I write a lot of Haskell. 00:00:47.070 --> 00:00:47.550 >> Good start. 00:00:48.019 --> 00:00:48.530 >> Yeah. 00:00:49.910 --> 00:00:50.360 I don't know. 00:00:50.360 --> 00:00:51.769 You caught me off guard here, Taylor. 00:00:54.555 --> 00:00:57.255 >> Well, uh, then let me say some things that I know about you, so 00:00:57.585 --> 00:00:58.815 >> you're better prepared than I am here. 00:00:59.115 --> 00:01:01.505 >> In addition to writing a lot of Haskell, you write 00:01:01.505 --> 00:01:03.095 a lot of Haskell content. 00:01:03.095 --> 00:01:07.625 You've authored two books, uh, thinking with types and algebra driven design. 00:01:08.015 --> 00:01:10.835 Uh, neither of which I think are necessarily like Haskell 00:01:10.835 --> 00:01:14.615 books, quote unquote, but they do sort of intersect quite a bit. 00:01:15.425 --> 00:01:16.685 >> Yeah, I think that's very fair. 00:01:17.075 --> 00:01:20.855 >> And, uh, you also author the blog reasonably polymorphic. 00:01:21.240 --> 00:01:25.259 And, uh, you're the author of the polysemy am I saying that, right? 00:01:25.740 --> 00:01:25.950 >> Yeah. 00:01:25.950 --> 00:01:31.320 >> Polysemy library for, uh, what's that like freer effects effect system. 00:01:32.490 --> 00:01:32.850 >> Yeah. 00:01:32.850 --> 00:01:34.200 Some sort of weird effect system. 00:01:37.050 --> 00:01:39.780 >> Uh, and more recently you've been working on wing man 00:01:39.780 --> 00:01:44.550 for Haskell, which is a tool for, I would say program synthesis, maybe. 00:01:45.330 --> 00:01:45.630 >> Yeah. 00:01:45.630 --> 00:01:48.030 That's a, that's a great description of it. 00:01:48.990 --> 00:01:50.460 >> So you're telling me it's not. 00:01:50.895 --> 00:01:55.815 Like the apex weapon, the wing man, you know, is that it? 00:01:56.315 --> 00:01:57.015 >> No, it's not. 00:01:57.035 --> 00:02:00.185 I really wanted to call it copilot, but that one's turned out to already be used. 00:02:00.725 --> 00:02:01.145 >> Really? 00:02:01.625 --> 00:02:01.955 >> Yeah. 00:02:01.955 --> 00:02:02.914 >> What's called copilot 00:02:03.335 --> 00:02:03.604 >> there's. 00:02:03.604 --> 00:02:08.375 Um, there's like a NASA DSL for doing like verified C plus 00:02:08.375 --> 00:02:09.875 plus programs or something. 00:02:10.384 --> 00:02:11.404 Not quite the same thing. 00:02:11.404 --> 00:02:11.825 No. 00:02:11.885 --> 00:02:14.165 Um, but it's a great name and I'm upset that they got it. 00:02:16.075 --> 00:02:17.034 >> Well, wing man is good too. 00:02:17.034 --> 00:02:17.695 I like that. 00:02:17.904 --> 00:02:18.325 >> Thank you. 00:02:18.744 --> 00:02:20.454 >> Um, so maybe let's launch into that. 00:02:20.454 --> 00:02:22.105 Could you tell us a little about wingman? 00:02:22.105 --> 00:02:22.704 What does it do? 00:02:23.244 --> 00:02:23.575 >> Sure. 00:02:23.635 --> 00:02:28.494 Um, so wingman is a plugin for the Haskell language server and the 00:02:28.494 --> 00:02:34.045 idea is it tries to automate away, um, the like ho hold driven design. 00:02:34.489 --> 00:02:37.039 Um, philosophy where you, you say, like, I don't really know the code I'm 00:02:37.039 --> 00:02:38.389 writing, I'm going to put it in a hole. 00:02:38.569 --> 00:02:41.179 And then the compiler tells you what that hole has type. 00:02:41.209 --> 00:02:41.449 Right. 00:02:41.449 --> 00:02:42.289 It gives you the type of it. 00:02:42.289 --> 00:02:46.159 And then you say, okay, well I know this thing has some type and I sort of know 00:02:46.159 --> 00:02:48.499 roughly what type I think it should be. 00:02:48.499 --> 00:02:51.109 So you, maybe you put an fmap in and then you put it in another hole 00:02:51.469 --> 00:02:54.649 and then it says, okay, well now the hole has changed because you've sort 00:02:54.649 --> 00:02:55.999 of synthesize some of the program. 00:02:56.719 --> 00:03:02.315 Um, and for a lot of code code, this turns out to like, Really 00:03:02.345 --> 00:03:05.345 what you're doing is just typing in the things GHC tells you to type. 00:03:05.644 --> 00:03:05.945 >> Yeah. 00:03:06.334 --> 00:03:06.484 >> Right. 00:03:06.484 --> 00:03:07.565 >> And it's, it's a little silly, right. 00:03:07.565 --> 00:03:08.825 So I thought, why not? 00:03:08.855 --> 00:03:10.084 Why don't we just automate that? 00:03:10.325 --> 00:03:10.535 Right. 00:03:10.535 --> 00:03:13.265 Why don't we just automate that conversation with the compiler and 00:03:13.415 --> 00:03:16.774 see if we can synthesize all sorts of the dumb programs that you would write 00:03:16.774 --> 00:03:19.505 yourself if you just follow the holes. 00:03:19.945 --> 00:03:20.214 >> Yeah. 00:03:20.424 --> 00:03:22.464 Uh, we do that surprisingly often here. 00:03:22.494 --> 00:03:26.195 Uh, We haven't been able to get HLS to work reliably on our code base, 00:03:26.225 --> 00:03:30.364 unfortunately, but we do the, like put a typed hole in there and then copy paste 00:03:30.364 --> 00:03:32.554 or just type in whatever GHC suggests. 00:03:33.154 --> 00:03:35.105 If there's only one thing often there are multiple, you know, and 00:03:35.105 --> 00:03:36.965 then you pick the right one, the one that's probably not, mempty. 00:03:36.965 --> 00:03:38.214 >> It always suggests unsafe coerce. 00:03:38.334 --> 00:03:38.545 >> Yeah. 00:03:38.855 --> 00:03:40.165 >> Wingman doesn't do that, thankfully. 00:03:40.765 --> 00:03:43.105 >> The trick is to not have that one in scope, I think. 00:03:43.285 --> 00:03:47.454 But yeah, we get mempty a lot or like const or something like that. 00:03:47.575 --> 00:03:48.325 >> Yeah, absolutely. 00:03:48.725 --> 00:03:52.084 >> Um, but yeah, it is kind of silly to be doing this copy pasting, 00:03:52.144 --> 00:03:55.265 and it sounds like wingman automates some of that, but also I got the 00:03:55.265 --> 00:03:59.135 impression that, that it does more than just naively filling in the 00:03:59.135 --> 00:04:01.265 whole, the GHC suggests is that right? 00:04:01.855 --> 00:04:04.285 >> Um, yeah, so there, there's sort of two things there. 00:04:04.285 --> 00:04:07.165 One of which is, uh, we have this, this like proof search 00:04:07.195 --> 00:04:08.184 going on in the background. 00:04:08.184 --> 00:04:12.594 And so it's actually trying to find a good program, um, by, 00:04:12.744 --> 00:04:13.915 for some definition of good. 00:04:13.915 --> 00:04:14.124 Right. 00:04:14.124 --> 00:04:17.755 And that sort of usually if you write code, um, you'll. 00:04:18.904 --> 00:04:20.944 Often, if you like see code that a beginner is written, 00:04:21.005 --> 00:04:22.564 they'll like, it'll be crazy. 00:04:22.564 --> 00:04:25.235 And like the type signature doesn't really correspond to the definition. 00:04:25.235 --> 00:04:28.324 And it's sort of hard to put your hand on what that means. 00:04:28.865 --> 00:04:33.095 Um, but so, so like a good metric for that is sort of linearity. 00:04:33.095 --> 00:04:37.084 You want generally your variables to only be used once, right. 00:04:38.005 --> 00:04:41.755 A program where if you can synthesize a solution only uses your variables 00:04:41.755 --> 00:04:44.694 once that's usually better than one that uses the multiple times. 00:04:44.934 --> 00:04:45.174 >> Right. 00:04:46.505 --> 00:04:47.794 >> Or not at all right, exactly. 00:04:47.794 --> 00:04:50.525 Which is the const the unsafe course sort of solution. 00:04:50.914 --> 00:04:54.875 Um, so that is sort of the, the interesting part of it. 00:04:54.934 --> 00:04:59.464 Um, and then we also have a bunch of like ergonomic things going on. 00:04:59.464 --> 00:05:02.044 And so, um, Wingman, we'll also do things like case splitting. 00:05:02.044 --> 00:05:06.034 And so you can say, um, Hey, I want you to case split on X and that 00:05:06.034 --> 00:05:11.044 is some weird ADT and it'll, um, it'll like multiply out every match. 00:05:11.074 --> 00:05:14.794 So you'll get multiple definitions of the function for every possible constructor. 00:05:15.574 --> 00:05:15.875 Right. 00:05:15.875 --> 00:05:19.895 So that's, that turns like one typed hole into many potentially. 00:05:19.895 --> 00:05:20.135 Right. 00:05:20.135 --> 00:05:21.655 And then you keep on filling and from there 00:05:22.074 --> 00:05:22.375 it will. 00:05:22.405 --> 00:05:22.645 Yeah. 00:05:23.365 --> 00:05:23.574 >> Hmm. 00:05:23.635 --> 00:05:23.964 >> Cool. 00:05:24.204 --> 00:05:28.974 And you mentioned linearity, uh, I don't want to go too far off on a tangent 00:05:28.974 --> 00:05:33.865 here, but I'm wondering, is there with linear types landed in GHC nine? 00:05:33.865 --> 00:05:37.584 Is there an opportunity for wingman to make use of that information 00:05:37.584 --> 00:05:41.064 and say, okay, I know that this needs to be used, so therefore 00:05:41.064 --> 00:05:42.714 that's going to guide my synthesis. 00:05:43.414 --> 00:05:45.395 >> Uh, that is a good question. 00:05:45.995 --> 00:05:50.554 I have not even looked at the linear stuff, um, even in the language. 00:05:50.554 --> 00:05:56.245 So, uh, um, but yeah, the way it works is it's using all of 00:05:56.245 --> 00:05:57.745 the information from GHC itself. 00:05:58.164 --> 00:06:02.694 And so, um, presumably GHC will tell me about the multiplicity of my arrows. 00:06:02.755 --> 00:06:05.694 And then, um, the trick is just to run the proof search sets 00:06:05.694 --> 00:06:08.155 that, such that it respects that. 00:06:08.184 --> 00:06:10.944 So I don't think there'd be any challenges there other than just writing the code. 00:06:11.515 --> 00:06:11.755 >> Cool. 00:06:12.709 --> 00:06:15.650 And I mean, Wingman could probably write some of that code for you, right? 00:06:16.760 --> 00:06:19.780 >> Like the more like the better it gets, the more I use it in daily 00:06:19.780 --> 00:06:22.809 dogfooding and, um, it's remarkable. 00:06:22.839 --> 00:06:26.169 How, how much, like, just how lovely it is, right. 00:06:26.169 --> 00:06:29.769 Compared to the bad old days where I had to write a case statement for myself and 00:06:29.769 --> 00:06:31.540 like, go look up all the constructors. 00:06:31.849 --> 00:06:32.070 Right. 00:06:32.070 --> 00:06:34.629 It's sort of stupid how, how much work that was. 00:06:34.629 --> 00:06:38.710 And I didn't realize because, um, just like the IDE situation 00:06:38.710 --> 00:06:39.969 was so bad for Haskell that. 00:06:40.400 --> 00:06:43.430 Um, like before Haskell language server, you just, it wasn't 00:06:43.430 --> 00:06:45.050 worth your time often to do it. 00:06:45.290 --> 00:06:45.710 Right. 00:06:45.800 --> 00:06:48.420 So it's, it's an amazing change in the last year. 00:06:48.499 --> 00:06:52.280 So the HLS guys are amazing and I wanted to thank you so much. 00:06:52.420 --> 00:06:55.599 >> Yeah, well, like I mentioned, we haven't been able to get it working 00:06:55.599 --> 00:06:59.170 reliably with our code base, but uh, many of us have been working with it 00:06:59.170 --> 00:07:03.520 in our like side projects or whatever, and everyone that has it working just 00:07:03.520 --> 00:07:04.690 immediately falls in love with it. 00:07:04.690 --> 00:07:05.229 It's amazing. 00:07:05.810 --> 00:07:08.300 >> Yeah, it really adds a lot to the language. 00:07:09.710 --> 00:07:09.940 >> Yeah. 00:07:10.239 --> 00:07:14.739 We've been kind of waiting for this to come to the ecosystem because we've been 00:07:15.190 --> 00:07:20.200 kind of stranded as far as, you know, tools that we have in our tool belt. 00:07:20.590 --> 00:07:26.859 Um, and I think agile HLS really just, you know, hit a home, run more or less 00:07:26.859 --> 00:07:32.379 for the usability and feature fullness that we need in the Haskell community. 00:07:33.080 --> 00:07:34.009 >> Yeah, absolutely. 00:07:34.070 --> 00:07:35.810 It's it's been like day and night. 00:07:35.810 --> 00:07:38.749 Just how quickly the tooling situation has changed the last year. 00:07:39.070 --> 00:07:39.369 >> Yeah. 00:07:39.580 --> 00:07:43.599 And it's funny when we were talking to Matt Parsons a couple of weeks ago, he 00:07:43.599 --> 00:07:48.310 mentioned that since Haskell is such a powerful language, you can kind of 00:07:48.310 --> 00:07:50.659 get away without having a powerful IDE. 00:07:51.099 --> 00:07:55.269 Uh, but once you also have a powerful idea, you just kind of 00:07:55.269 --> 00:07:56.999 like leapfrog your own productivity. 00:07:57.099 --> 00:07:57.969 It's great. 00:07:58.539 --> 00:07:59.080 >> It's crazy. 00:07:59.080 --> 00:07:59.409 Yeah. 00:08:00.575 --> 00:08:04.295 >> Um, so could you tell us, uh, how did you come to work on 00:08:04.354 --> 00:08:05.705 wing man and program synthesis? 00:08:05.705 --> 00:08:06.425 What drew you to that? 00:08:07.285 --> 00:08:08.754 >> Yeah, that's a, that's a great question. 00:08:08.785 --> 00:08:13.104 Um, I, so maybe two years ago I sort of fed up. 00:08:13.134 --> 00:08:16.224 I was living in Ottawa in Canada, which was an atrocious place and 00:08:16.224 --> 00:08:20.364 just sort of missing a lot of the intellectual community I was looking for. 00:08:20.844 --> 00:08:23.825 And so I decided I was just going to like run away and live on Haskeller's 00:08:23.844 --> 00:08:25.945 couches for as long as I could handle. 00:08:26.394 --> 00:08:26.604 >> Yeah. 00:08:26.695 --> 00:08:27.175 I remember that. 00:08:27.175 --> 00:08:27.565 >> So. 00:08:28.070 --> 00:08:28.400 Yeah. 00:08:28.430 --> 00:08:30.950 So I made it for about four months of like couch surfing and meeting 00:08:30.950 --> 00:08:32.539 all sorts of really amazing people. 00:08:32.930 --> 00:08:37.280 Um, and one of the people I met was James King, who had like a little tablet. 00:08:37.370 --> 00:08:42.170 Um, and he, he was sort of pitching me on this idea of programming on the tablet. 00:08:42.559 --> 00:08:42.770 Right. 00:08:42.770 --> 00:08:43.250 And I'm like, what? 00:08:43.250 --> 00:08:45.140 Like, what would you need to do to make that happen? 00:08:45.755 --> 00:08:49.474 Um, so w the dream I have is like one day being able to be out in 00:08:49.474 --> 00:08:54.214 the park, on my tablet, and like programming, like productively out in 00:08:54.214 --> 00:08:57.035 the park without a keyboard, without a monitor, without any of that crap. 00:08:57.035 --> 00:08:57.365 Right. 00:08:58.835 --> 00:09:03.425 Um, and so that, that question sort of got me thinking about like how, how could we 00:09:03.454 --> 00:09:07.385 find a better interface for programming that isn't just typing on a keyboard? 00:09:07.625 --> 00:09:07.925 >> Right. 00:09:08.525 --> 00:09:12.725 >> Um, at the same time, I, I was talking a lot with the Reed Mullanix who 00:09:13.055 --> 00:09:18.335 has been working on a tactic synthesizer for Haskell and sort of, he does a lot of. 00:09:18.800 --> 00:09:22.520 Things in like dependently type languages where, um, they have all the 00:09:22.530 --> 00:09:26.400 sort of this code synthesis stuff, and he wanted to bring that into Haskell. 00:09:26.600 --> 00:09:29.390 And so he had built like a bunch of really incredible libraries, 00:09:29.480 --> 00:09:32.600 um, that do most of the work. 00:09:33.170 --> 00:09:38.290 And so really my contribution was taking the, the idea and trying 00:09:38.440 --> 00:09:40.780 to bridge the gap there, right. 00:09:40.780 --> 00:09:43.030 Between the interface and the solution. 00:09:43.630 --> 00:09:43.990 >> Okay. 00:09:44.230 --> 00:09:49.550 >> Um, yeah, so that's sorta how I got started on it was just, um, This 00:09:49.550 --> 00:09:53.180 like, sort of being tired of being on a bus and trying to type yeah. 00:09:53.180 --> 00:09:55.790 Like having terrible RSI for the week after, you know? 00:09:56.240 --> 00:09:56.510 >> Yeah. 00:09:57.099 --> 00:10:00.849 Um, it's funny, you mentioned different, uh, like using a tablet as sort of 00:10:00.849 --> 00:10:05.020 a different programming paradigm and I've thought a lot about that as well. 00:10:05.020 --> 00:10:08.260 I imagine a lot of programmers have of like, why is it that I have to 00:10:08.260 --> 00:10:11.650 be sitting here with a full-size keyboard in order to be productive? 00:10:12.160 --> 00:10:13.319 Um, and yeah. 00:10:13.895 --> 00:10:17.464 It seems like the interface for a tablet would be wildly different or like in 00:10:17.464 --> 00:10:22.115 VR or on a phone or really anywhere but sitting at a desk with a computer. 00:10:22.115 --> 00:10:22.204 >> Right. 00:10:22.855 --> 00:10:26.365 I think the value of a keyboard is that it lets you type arbitrary strings. 00:10:26.365 --> 00:10:26.635 Right. 00:10:26.635 --> 00:10:29.875 But almost no strings are programs. 00:10:30.055 --> 00:10:30.444 >> Yeah. 00:10:30.805 --> 00:10:31.075 >> Right. 00:10:31.135 --> 00:10:33.954 It's sort of ridiculous that we even use strings to represent 00:10:33.954 --> 00:10:34.944 these things in the first place. 00:10:35.035 --> 00:10:35.425 >> Right. 00:10:35.575 --> 00:10:39.504 And a lot of the strings that you end up typing, aren't arbitrary, they come 00:10:39.504 --> 00:10:41.004 from some other part of your code base. 00:10:41.300 --> 00:10:41.839 >> That's true. 00:10:41.869 --> 00:10:42.200 Yeah. 00:10:42.230 --> 00:10:46.490 Um, even like, like keywords are, should be auto completable and like a lot of 00:10:46.490 --> 00:10:49.160 keywords you need in like together. 00:10:49.430 --> 00:10:51.890 So I need to, every time I have a case, I need the word of 00:10:52.040 --> 00:10:52.579 >> exactly. 00:10:52.760 --> 00:10:53.810 >> So why do I have to take that? 00:10:54.109 --> 00:10:54.290 >> Yeah. 00:10:54.349 --> 00:10:54.650 >> Right. 00:10:54.859 --> 00:10:57.260 At any given point, there's only like five things you might want to do. 00:10:58.280 --> 00:10:58.579 Right. 00:10:58.579 --> 00:11:00.530 So why don't we just give you those options? 00:11:00.940 --> 00:11:01.510 >> I like it. 00:11:01.690 --> 00:11:06.099 Um, and I know a lot of people go down the route of structured editing as a, 00:11:06.579 --> 00:11:09.819 you know, solution to this problem of, instead of typing text into an editor, 00:11:10.099 --> 00:11:13.819 Let's have something like, I think scratch is kind of the prototypical example, 00:11:13.819 --> 00:11:17.210 but, you know, block-based where you pull that case statement out of some 00:11:17.210 --> 00:11:18.649 pallet and drop it in your program. 00:11:19.159 --> 00:11:23.089 What, how did you, or what kind of led you to program synthesis 00:11:23.119 --> 00:11:24.349 versus structured editing? 00:11:25.149 --> 00:11:27.970 >> I think structured editing is a good approach. 00:11:28.089 --> 00:11:30.310 Um, I didn't know how to do that. 00:11:32.680 --> 00:11:35.800 Um, and I guess the other thing is like, even if you are, even if 00:11:35.800 --> 00:11:36.879 you have a better interface, like. 00:11:37.235 --> 00:11:40.954 Still, why do I have to code things that have exactly one solution, right, 00:11:40.975 --> 00:11:41.275 >> right. 00:11:41.795 --> 00:11:42.365 >> A huge purse. 00:11:42.395 --> 00:11:45.935 Like part of the reason I like Haskell is the type system is so 00:11:45.935 --> 00:11:47.555 good at constraining implementations. 00:11:48.305 --> 00:11:48.605 Right. 00:11:48.635 --> 00:11:50.975 And so I sort of look at like, you've done your job. 00:11:51.005 --> 00:11:53.825 Well, if, if there's exactly one solution to your type, 00:11:54.125 --> 00:11:54.365 >> right. 00:11:54.395 --> 00:11:56.045 >> That means you've designed a good program. 00:11:56.045 --> 00:11:58.415 And then let's just find that thing. 00:11:59.875 --> 00:12:00.415 >> I like that. 00:12:00.895 --> 00:12:00.985 Yeah. 00:12:00.985 --> 00:12:01.315 That's good. 00:12:01.315 --> 00:12:04.464 Cause I'm trying to imagine, like in JavaScript, what would 00:12:04.464 --> 00:12:05.755 program synthesis look like? 00:12:05.785 --> 00:12:06.115 And. 00:12:06.575 --> 00:12:08.375 It seems like, yeah. 00:12:08.405 --> 00:12:08.855 I don't know. 00:12:08.944 --> 00:12:09.875 I don't know enough about it. 00:12:10.474 --> 00:12:10.865 >> Yeah. 00:12:11.135 --> 00:12:12.694 I'm not without crazy AI. 00:12:12.994 --> 00:12:13.265 >> Yeah. 00:12:13.295 --> 00:12:15.365 Or maybe with TypeScript, there might be enough ins there. 00:12:15.815 --> 00:12:16.085 >> Yeah. 00:12:16.085 --> 00:12:16.444 I dunno. 00:12:17.015 --> 00:12:20.525 >> Um, actually we use a plugin called, uh, tab nine. 00:12:20.839 --> 00:12:23.000 That does a much, Oh, are you familiar with it? 00:12:23.389 --> 00:12:25.010 >> Uh, I, I sort of know it exists. 00:12:25.040 --> 00:12:26.930 It's sort of like machine learning. 00:12:27.409 --> 00:12:28.040 >> Yeah. 00:12:28.159 --> 00:12:30.290 It's very, I don't know how to describe it. 00:12:30.290 --> 00:12:34.159 Maybe like stochastic, where it just looks at the strings in your code base 00:12:34.190 --> 00:12:36.260 and figures out how often they occur. 00:12:36.500 --> 00:12:39.109 And then when you start typing something, it's like, Oh, normally when 00:12:39.109 --> 00:12:41.930 this is before the cursor and you're typing this, this is what comes after. 00:12:41.930 --> 00:12:43.190 So it'll suggest that it 00:12:43.190 --> 00:12:43.730 >> Dies it work well. 00:12:44.569 --> 00:12:44.990 >> Pretty well. 00:12:44.990 --> 00:12:49.339 Yeah, especially for pretty rote stuff like imports or again, HLS 00:12:49.339 --> 00:12:51.800 solves imports where you, but if you are typing one out, it'll be 00:12:51.800 --> 00:12:53.150 like, this is a typical module name. 00:12:53.230 --> 00:12:53.680 Here you go. 00:12:54.069 --> 00:12:54.280 >> Cool. 00:12:55.690 --> 00:12:59.110 >> Yeah, it'd be nice to get the more time invested in 00:12:59.260 --> 00:13:03.190 figuring out how to make HLS work in our program, but for the time 00:13:03.240 --> 00:13:04.450 >> Do you use a lot of template Haskell. 00:13:05.420 --> 00:13:08.750 >> We have a little bit where you're using more storage, we've turned 00:13:08.750 --> 00:13:12.620 toward using more of the persistent, uh, quasi quoter for doing our models. 00:13:12.670 --> 00:13:13.890 So yeah, that's 00:13:14.170 --> 00:13:16.000 >> often that that's the big issue. 00:13:16.720 --> 00:13:20.170 Um, and if you can sort of separate that into a different package, I 00:13:20.170 --> 00:13:21.550 suspect that will solve your problems. 00:13:21.550 --> 00:13:22.510 But I can't promise 00:13:23.560 --> 00:13:26.920 >> we have somewhat, I mean, like everybody, we have a bespoke environment 00:13:26.920 --> 00:13:29.410 and we got Docker containers and we got all kinds of stuff going on. 00:13:29.500 --> 00:13:30.010 >> Of course. 00:13:30.940 --> 00:13:32.770 >> Um, but yeah, cam you use tab nine. 00:13:32.770 --> 00:13:33.579 I think more than I do. 00:13:33.980 --> 00:13:36.770 Ah, so you may be able to speak to like what it does, what it's good at. 00:13:37.190 --> 00:13:38.599 Especially in comparison to HLS. 00:13:39.079 --> 00:13:39.560 >> Yeah. 00:13:39.589 --> 00:13:44.659 I mean, if you're making a sweeping code change across the entire code 00:13:44.659 --> 00:13:49.339 base, it can pretty much figure out what you're trying to type as you, 00:13:49.430 --> 00:13:50.480 you know, just kind of start it. 00:13:50.510 --> 00:13:52.250 So it's been really helpful. 00:13:52.310 --> 00:13:57.139 Um, you know, imports is one that is obviously, it has a lot of examples to 00:13:57.230 --> 00:14:00.230 analyze and say, Hey, this is what we think you're doing, especially because 00:14:00.230 --> 00:14:03.079 we have pretty consistent naming schemes. 00:14:03.109 --> 00:14:04.159 So it makes it really easy. 00:14:04.520 --> 00:14:10.550 Um, And, uh, you know, when you're writing function definitions, it can 00:14:10.550 --> 00:14:14.060 get a little tricky sometimes because it wants you to, like, if you're doing your 00:14:14.060 --> 00:14:16.940 type signature, like the next line, it tries to say, Oh, you're doing your type 00:14:16.940 --> 00:14:20.209 signature . Again, and you're like, wait, no, I'm not actually implemented here. 00:14:20.209 --> 00:14:23.360 So that can get a little bit of a note and a little bit of 00:14:23.360 --> 00:14:24.500 annoyance there, but right. 00:14:24.800 --> 00:14:27.860 Overall it's pretty helpful. 00:14:27.949 --> 00:14:33.709 Uh, just in the day to day, you know, I think if we can get some HLS love, then. 00:14:34.094 --> 00:14:38.594 Yeah, that sh meet the need for, that could go away, um, to be really cool. 00:14:39.425 --> 00:14:39.814 >> It's funny. 00:14:39.814 --> 00:14:44.735 Cause they're kind of, uh, similar solutions to, or sorry they're 00:14:44.735 --> 00:14:47.615 approaching the same problem with radically different solutions. 00:14:47.615 --> 00:14:48.755 One is like very smart. 00:14:48.755 --> 00:14:50.765 Give me as much information from the compiler and I'll use it. 00:14:50.765 --> 00:14:53.555 And the other is like, I don't need to know even what language you're typing. 00:14:53.555 --> 00:14:54.094 I'll just guess 00:14:55.865 --> 00:14:57.964 >> it's, it's amazing to me that that works at all. 00:14:57.995 --> 00:14:58.145 >> Yeah. 00:14:58.175 --> 00:14:58.415 Yeah. 00:14:58.865 --> 00:14:59.584 It is startling. 00:15:00.035 --> 00:15:01.865 Um, so yeah, try that out. 00:15:01.895 --> 00:15:03.714 And uh, I'd be curious to see what you think about it. 00:15:04.124 --> 00:15:08.624 Um, but on the topic of program synthesis, I am aware of a couple earlier attempts 00:15:08.624 --> 00:15:10.334 with Haskell to synthesize programs. 00:15:10.364 --> 00:15:12.044 Like I think Lambda bot can do some stuff. 00:15:12.074 --> 00:15:15.374 And there's a package called djinn that does something similar is 00:15:15.374 --> 00:15:17.504 wing man built on top of those are related to them in any way. 00:15:17.614 --> 00:15:18.004 >> Not at all. 00:15:18.004 --> 00:15:20.914 No, I don't know how Lambda button does it, but I know djinn um, 00:15:21.364 --> 00:15:23.254 doesn't work particularly well. 00:15:23.824 --> 00:15:24.474 >> I've never used it. 00:15:24.774 --> 00:15:25.584 I just know it exists. 00:15:25.584 --> 00:15:26.464 Djinn will do a lot 00:15:26.464 --> 00:15:33.344 >> of like, um, Like sort of const stuff like it doesn't care if it's used 00:15:33.344 --> 00:15:34.994 arguments is just like, here's a solution. 00:15:35.084 --> 00:15:38.114 Um, one thing that we meant also does that Djinn doesn't is recursion. 00:15:39.104 --> 00:15:44.384 And so Djinn or, uh, Wingman can like implement foldr for you, for example. 00:15:44.534 --> 00:15:48.854 Um, and if it, if it does recursion that guarantees that, um, it's, 00:15:48.854 --> 00:15:51.254 recursing on something structurally smaller, so it will terminate 00:15:51.254 --> 00:15:51.675 >> productive. 00:15:51.704 --> 00:15:51.974 Yeah. 00:15:52.319 --> 00:15:53.130 >> Yeah, exactly. 00:15:53.250 --> 00:15:57.719 Um, so Djinn I think is it's, it's interesting that exists and sort of, 00:15:57.719 --> 00:16:00.810 it was inspiring to me just to see that someone had made progress there. 00:16:00.810 --> 00:16:04.530 But, um, if you've ever like tried to use it for real, it, 00:16:04.589 --> 00:16:06.180 it falls short quite soon. 00:16:06.709 --> 00:16:06.979 >> Mm. 00:16:08.270 --> 00:16:09.349 >> Well, I hadn't tried to use it. 00:16:09.380 --> 00:16:12.229 I don't think it builds with more recent GHC so that's what 00:16:12.410 --> 00:16:13.520 prevented me from trying it out. 00:16:13.520 --> 00:16:13.579 Yeah. 00:16:13.964 --> 00:16:16.154 >> There's um, there's another thing I've heard of called magic 00:16:16.154 --> 00:16:20.114 Haskell, which is sort of the other way is it says here's some arguments 00:16:20.114 --> 00:16:21.194 and here's what the output should be. 00:16:21.194 --> 00:16:24.584 And it tries to synthesize a function that produces the outputs from the inputs. 00:16:24.644 --> 00:16:25.244 >> Oh, that's cool. 00:16:25.244 --> 00:16:27.284 So more kind of spec based. 00:16:27.344 --> 00:16:28.244 >> Yeah, exactly. 00:16:28.274 --> 00:16:31.094 Um, I haven't, I haven't looked at it with the website was down 00:16:31.094 --> 00:16:32.295 when I tried to run it, but 00:16:32.624 --> 00:16:33.404 >> that sounds really cool. 00:16:33.694 --> 00:16:33.814 Yeah. 00:16:33.844 --> 00:16:35.134 I've heard of similar projects. 00:16:35.974 --> 00:16:39.154 Um, I th I think I I'm trying to remember the name. 00:16:39.154 --> 00:16:41.344 There was a project in like scheme or something like that. 00:16:42.224 --> 00:16:45.284 I think it was called barley man, or it's been many years since I heard. 00:16:45.314 --> 00:16:48.674 Anyway, there was some presentation where it's like, you, you give a test case and 00:16:48.734 --> 00:16:50.804 it'll produce a function that meets that. 00:16:50.804 --> 00:16:53.294 And then you add another test case and it'll churn for a bit and say, 00:16:53.294 --> 00:16:54.554 okay, well I have a new function now. 00:16:54.944 --> 00:16:58.034 And as you add more and more test cases, uh, the implementation gets 00:16:58.034 --> 00:17:01.864 more and more, you know, don't look behind the curtain type implementation, 00:17:01.874 --> 00:17:03.214 but well, it works technically, 00:17:04.324 --> 00:17:05.974 >> at least it gives you the outputs for the inputs. 00:17:05.974 --> 00:17:06.185 Right, 00:17:06.264 --> 00:17:06.474 >> right. 00:17:06.665 --> 00:17:06.935 Yeah. 00:17:06.935 --> 00:17:12.435 And then, um, I think for those, that type of program synthesis, uh, Property-based 00:17:12.435 --> 00:17:16.785 tests will give you much more assurance that your implementation isn't something 00:17:16.785 --> 00:17:18.285 more than just a pile of this statements. 00:17:18.285 --> 00:17:19.785 Like if you give me this, I'll give you that. 00:17:20.235 --> 00:17:23.474 Uh, which I think ties in with algebra diff driven design to 00:17:23.474 --> 00:17:24.555 kind of take a corner here. 00:17:24.615 --> 00:17:25.095 Um, 00:17:25.335 --> 00:17:25.964 >> that was a good segue. 00:17:26.255 --> 00:17:26.645 >> Thank you. 00:17:29.255 --> 00:17:32.165 So yeah, property-based tests are, you know, a way to. 00:17:34.259 --> 00:17:37.679 State properties that should hold in your system and then test it against 00:17:37.679 --> 00:17:38.999 the implementation and see if it works. 00:17:39.059 --> 00:17:43.829 And algebra driven design is all about coming up with those properties, right? 00:17:44.929 --> 00:17:45.439 >> Yeah. 00:17:45.469 --> 00:17:49.850 It's um, the, the book itself sort of the main thesis of it is that. 00:17:50.219 --> 00:17:52.139 If we're doing functional program, we should really be thinking 00:17:52.139 --> 00:17:53.580 about equality of programs. 00:17:53.759 --> 00:17:54.060 Right. 00:17:54.060 --> 00:17:56.340 That's sort of what it buys us over imperative stuff. 00:17:57.029 --> 00:18:02.129 And, um, and so if you're like designing some API, it's really interesting to 00:18:02.129 --> 00:18:07.590 ask when are two expressions in this like DSL or this API is the same. 00:18:07.620 --> 00:18:07.979 Right, 00:18:08.159 --> 00:18:08.489 >> right. 00:18:08.550 --> 00:18:10.340 >> And we're sort of used to this in everyday Haskel. 00:18:10.629 --> 00:18:13.270 We say like fmap dot fmap is the same as one fmap. 00:18:13.830 --> 00:18:14.159 Right. 00:18:14.865 --> 00:18:19.665 Um, but very often, like very rarely do you see people think about this for like 00:18:19.665 --> 00:18:24.885 the libraries they're writing and lesser, the category theory, people and stuff. 00:18:25.245 --> 00:18:31.335 Um, and so the, the claim is that, um, we can think about equality for 00:18:31.335 --> 00:18:33.405 like very mundane sorts of tasks. 00:18:33.719 --> 00:18:34.069 Right. 00:18:34.110 --> 00:18:37.769 Like very mundane, like real world applications that you're writing. 00:18:37.860 --> 00:18:39.840 Um, they, they should have equalities as well. 00:18:40.469 --> 00:18:44.759 And, um, so, so there's a few things that come from that, right? 00:18:44.759 --> 00:18:48.809 One of which is if you have these equalities, then of course you can 00:18:48.809 --> 00:18:52.289 turn them into property tests, and then it gives you like wicked amounts 00:18:52.350 --> 00:18:54.689 of, of just test coverage, right? 00:18:54.689 --> 00:18:57.689 For every property test, you can generate arbitrary many unit tests. 00:18:58.559 --> 00:19:03.179 Um, And so that's, that's exciting, but the other thing is what it does, is it 00:19:03.179 --> 00:19:05.659 constrains your implementation, right? 00:19:05.990 --> 00:19:09.590 Um, there's going to be sort of infinite, many ways of implementing a 00:19:09.590 --> 00:19:14.570 program, such that like all of these equality's hold, but often if you like 00:19:14.600 --> 00:19:18.230 chase the equalities, you can find different ways of representing programs. 00:19:18.620 --> 00:19:22.399 And so you can, you can use the equalities as a tool for as an 00:19:22.399 --> 00:19:25.459 implementer to say, like, I know that these two things are equivalent, 00:19:25.459 --> 00:19:27.050 but one of them is maybe faster. 00:19:27.629 --> 00:19:27.820 >> Right. 00:19:27.840 --> 00:19:30.540 >> So I'm going to choose that as my sort of basis. 00:19:30.929 --> 00:19:34.469 Um, and then use the, the qualities to rewrite all the things that user writes 00:19:34.500 --> 00:19:38.939 in a language that's, um, like useful to them, or make sense to them in a 00:19:38.939 --> 00:19:41.219 way that is equivalent, but faster. 00:19:41.459 --> 00:19:41.699 >> Right. 00:19:42.199 --> 00:19:42.379 Okay. 00:19:42.439 --> 00:19:46.580 That sounds to me, that sounds to me like something that is very 00:19:46.580 --> 00:19:48.409 appealing to programmers, especially. 00:19:48.779 --> 00:19:53.249 I feel like this comes up a lot in like lisp programming, where people want a 00:19:53.249 --> 00:19:57.899 very small, like kernel of, uh, primitives and then build everything out of that. 00:19:58.319 --> 00:20:03.389 And it sounds like algebra driven design is trying to find, uh, maybe 00:20:03.389 --> 00:20:06.659 in kind of a roundabout way, find those primitives, uh, such that they 00:20:06.659 --> 00:20:09.330 meet all these properties and then you can shuffle them around behind the 00:20:09.330 --> 00:20:10.769 scenes to get a good implementation. 00:20:11.360 --> 00:20:12.110 >> Yeah, I think so. 00:20:12.169 --> 00:20:13.580 I think that's a very good way of phrasing it. 00:20:13.729 --> 00:20:16.279 Um, one thing I'd like to stress is just that the implementation doesn't 00:20:16.279 --> 00:20:17.989 need to be at all based on the kernels. 00:20:18.330 --> 00:20:18.659 Right, 00:20:18.870 --> 00:20:19.200 >> right. 00:20:19.230 --> 00:20:21.629 >> The kernels are for the user, but for the implementation, you 00:20:21.629 --> 00:20:25.740 can have all sorts of crazy, like, um, specialized primitives that 00:20:25.740 --> 00:20:29.100 make no sense and user lands, but that's okay because they're fast. 00:20:29.490 --> 00:20:30.840 As long as you can prove the equality. 00:20:30.840 --> 00:20:31.169 It's fine. 00:20:31.669 --> 00:20:34.159 >> And I think this ties in with something else you said from 00:20:34.159 --> 00:20:36.350 the book about abstraction, where. 00:20:37.695 --> 00:20:42.075 Programmers often think about abstraction as like hiding implementation details. 00:20:42.075 --> 00:20:46.645 And it does do that, but, uh, it seems to be more powerful when your abstraction 00:20:46.665 --> 00:20:51.705 is based on this algebra so that, you know, your abstraction can't leak because 00:20:51.735 --> 00:20:55.545 the entire, like the rules of the thing are based on the algebra you built. 00:20:55.754 --> 00:20:59.925 So the implementation kind of by definition does not matter. 00:21:00.885 --> 00:21:02.265 >> And I think that's it. 00:21:02.730 --> 00:21:03.330 Absolutely. 00:21:03.389 --> 00:21:05.850 I think too many people think about abstractions. 00:21:05.850 --> 00:21:10.189 Like put it in a module, I'll put it behind it. 00:21:11.000 --> 00:21:11.209 Right. 00:21:11.209 --> 00:21:14.810 Or like I'll re I'll pull out this implementation to its own function. 00:21:14.909 --> 00:21:17.720 It's like, that's not, um, there's a quote from Dijkstra I really like, 00:21:17.720 --> 00:21:21.919 which is that, uh, abstraction is not about being vague, but about 00:21:21.919 --> 00:21:24.620 creating a new semantic level at which you can be absolutely precise. 00:21:24.889 --> 00:21:25.220 >> Right? 00:21:25.520 --> 00:21:25.730 Hmm. 00:21:27.450 --> 00:21:27.780 Yeah. 00:21:27.840 --> 00:21:29.300 Uh, so yeah, yeah. 00:21:29.300 --> 00:21:32.480 I, uh, like I mentioned earlier, have not made it entirely through this book 00:21:32.480 --> 00:21:34.250 yet, but I'm really enjoying it so far. 00:21:34.250 --> 00:21:37.909 And it feels like it'll give me some tools for approaching problems, uh, 00:21:37.940 --> 00:21:44.720 particularly, um, taking the time before diving into implementation to think 00:21:44.720 --> 00:21:47.930 about the problem and kind of push on the boundaries of it and see where it can be 00:21:47.930 --> 00:21:52.250 broken down into simpler pieces, which is something that I've already seen, um, 00:21:52.490 --> 00:21:53.990 in the examples that you give, where. 00:21:54.930 --> 00:21:58.470 You talk about like, you can come up with a property and it may be very complicated 00:21:58.470 --> 00:22:03.060 in that suggests that you may have multiple things kind of mixed together 00:22:03.060 --> 00:22:06.240 there or complected to borrow the, you know, the rich Hickey speak there. 00:22:06.400 --> 00:22:06.690 >> Right. 00:22:06.930 --> 00:22:11.370 >> Um, and you would do well to pull those apart and then in doing so 00:22:11.370 --> 00:22:14.070 you might discover more properties about your program, or you might discover a 00:22:14.070 --> 00:22:17.370 simple, simpler way to implement it, or, you know, any number of things. 00:22:17.490 --> 00:22:20.129 So looking forward to continuing to explore that. 00:22:20.790 --> 00:22:24.629 >> Yeah, well, uh, I think it's a great book and I'd strongly recommend, it 00:22:25.909 --> 00:22:28.379 >> might just be a little bit biased, but I agree with you. 00:22:30.529 --> 00:22:33.830 Um, but yeah, that's not the only book you've written, right? 00:22:33.889 --> 00:22:37.009 You previously wrote another book called thinking with types. 00:22:37.159 --> 00:22:38.090 What is that one about? 00:22:38.790 --> 00:22:42.149 >> That one is about all of the, um, all the wonky stuff you need to 00:22:42.149 --> 00:22:43.739 do in order to do type level program. 00:22:43.760 --> 00:22:44.989 I mean, Haskell, right. 00:22:45.439 --> 00:22:49.939 Um, w it's sort of unfortunate, that's such a book as necessary, right? 00:22:49.939 --> 00:22:54.860 Because if you look at languages like Agda or, um, Coq like properly 00:22:54.860 --> 00:22:58.879 dependently type languages, there is no T type level programming. 00:22:58.879 --> 00:22:59.959 It's just programming, 00:23:00.080 --> 00:23:00.469 >> right. 00:23:00.899 --> 00:23:02.749 >> In Haskell it's, it's sort of ridiculous that we have 00:23:02.749 --> 00:23:05.330 this like constraint kind where. 00:23:05.699 --> 00:23:08.850 It's sort of a tool, but it's not really, but it's like a set of 00:23:08.850 --> 00:23:10.709 constraints, but it's not data dot set. 00:23:11.669 --> 00:23:11.999 Right. 00:23:11.999 --> 00:23:13.979 And it's like, why does this exist? 00:23:13.979 --> 00:23:14.310 Right. 00:23:15.060 --> 00:23:20.100 So, um, so thinking what types of sort of a collection of all the folklore that 00:23:20.100 --> 00:23:24.780 has existed about how to do dependently type stuff or like type level programming, 00:23:24.959 --> 00:23:29.699 more so than more generally, um, without sort of needing to go through and 00:23:30.209 --> 00:23:32.429 find all the resources for yourself, 00:23:32.610 --> 00:23:32.909 >> right. 00:23:33.794 --> 00:23:39.044 Yeah, I, uh, I often, w we have turned recently into using more, uh, servant 00:23:39.074 --> 00:23:43.875 the HTTP API library, which is very much implemented at the type level. 00:23:44.264 --> 00:23:49.125 And it definitely, uh, highlights some of the, I don't know, sharp edges 00:23:49.155 --> 00:23:52.064 on dealing with this type level of programming and Haskell, because you 00:23:52.064 --> 00:23:55.695 have to leave the very comfortable value level programming world. 00:23:55.980 --> 00:23:59.280 And deal with this entirely different world, which is kind of disorienting. 00:23:59.550 --> 00:24:00.870 >> It's the same, but it's different. 00:24:01.290 --> 00:24:01.650 >> Right. 00:24:02.580 --> 00:24:03.240 >> And annoyingly. 00:24:05.210 --> 00:24:05.620 >> Yeah. 00:24:07.050 --> 00:24:09.690 And there's all new terminology to worry about, you know, you got type 00:24:09.690 --> 00:24:14.040 families and data, you know, like just, I want to deal with functions 00:24:14.040 --> 00:24:15.210 and you know, the stuff that I know, 00:24:15.950 --> 00:24:16.400 >> right. 00:24:16.490 --> 00:24:16.730 Yeah. 00:24:16.730 --> 00:24:19.100 It's definitely a mind bender to some degree. 00:24:19.460 --> 00:24:25.280 Um, you know, as someone who's not as experienced in Haskell, like w. 00:24:25.560 --> 00:24:29.429 Walking into type families and type level programming. 00:24:30.120 --> 00:24:30.570 Definitely. 00:24:30.570 --> 00:24:33.720 I mean, it's been insightful and fun to learn, but it 00:24:33.720 --> 00:24:35.580 definitely took, took a minute. 00:24:35.610 --> 00:24:37.200 So, um, yeah. 00:24:37.260 --> 00:24:42.840 Appreciate you taking the time to gather some helpful resources for that. 00:24:43.169 --> 00:24:45.870 Um, that way people aren't bouncing around. 00:24:47.780 --> 00:24:48.379 What do I do? 00:24:48.379 --> 00:24:49.879 What a type families, how does this work? 00:24:50.235 --> 00:24:50.595 >> Yeah, 00:24:50.885 --> 00:24:54.165 >> as an experience Haskell, or it doesn't make my brain bend. 00:24:54.165 --> 00:24:54.915 I need less. 00:24:56.475 --> 00:24:57.675 It's it's just weird. 00:24:57.675 --> 00:25:00.705 And like every single time I need to repage all these 00:25:00.795 --> 00:25:02.475 arcane rules for how to do it. 00:25:02.955 --> 00:25:07.845 And, um, as I get older and wiser, I sort of, the more, I feel like maybe 00:25:07.845 --> 00:25:12.315 this is a bad approach and like, maybe we just shouldn't be doing these 00:25:12.315 --> 00:25:14.264 things except in like very, very small. 00:25:14.975 --> 00:25:15.395 >> Yeah. 00:25:15.575 --> 00:25:17.675 So do you feel like we should be. 00:25:18.074 --> 00:25:22.695 Pushing toward dependently typed languages, or we should be pushing 00:25:22.695 --> 00:25:25.995 toward more, like give up on the type level programming and 00:25:25.995 --> 00:25:27.284 focus on the value level stuff. 00:25:28.185 --> 00:25:30.705 >> Um, I think either of those would be okay, 00:25:31.604 --> 00:25:33.014 >> but we're kind of in the middle right now. 00:25:33.014 --> 00:25:33.824 And that's the problem. 00:25:34.125 --> 00:25:36.735 >> Um, I don't know what the dependent Haskell story is going 00:25:36.735 --> 00:25:37.995 to look like, but I'm hoping. 00:25:38.429 --> 00:25:43.590 It will just work in the way that like lean or Idris just works. 00:25:43.860 --> 00:25:44.159 Right. 00:25:44.580 --> 00:25:46.290 Um, I hope it is. 00:25:46.290 --> 00:25:51.090 I, I want to believe, but based on what the current types story 00:25:51.090 --> 00:25:53.429 is, I don't know if I feel it yet. 00:25:53.730 --> 00:25:54.750 I haven't internalized it. 00:25:55.260 --> 00:25:55.530 >> Yeah. 00:25:55.530 --> 00:25:59.085 I haven't, uh, Been following the dependent Haskell thread. 00:25:59.345 --> 00:26:01.725 I haven't played with really any dependent, uh, 00:26:01.754 --> 00:26:02.835 dependently typed languages. 00:26:02.835 --> 00:26:03.834 I'm aware of Idris. 00:26:03.855 --> 00:26:08.085 And every time I see a tweet pop up with it, I'm like, man, that looks pretty cool. 00:26:08.085 --> 00:26:09.014 I should check it out sometime. 00:26:09.615 --> 00:26:15.205 Um, But, uh, yeah, I'm not hopeful that Haskell as a language and 00:26:15.205 --> 00:26:18.465 community will be able to shift from not being dependently typed 00:26:18.465 --> 00:26:19.394 to being dependently typed. 00:26:19.394 --> 00:26:23.084 It seems like too much of a change, but, you know, maybe it will happen. 00:26:23.114 --> 00:26:27.165 And I think with, uh, linear types, that's a, that's a similar type of change. 00:26:27.495 --> 00:26:30.465 And maybe if that one goes really well, that could bode well for 00:26:30.465 --> 00:26:31.935 also doing dependent types. 00:26:32.405 --> 00:26:32.764 >> Yeah. 00:26:33.034 --> 00:26:36.064 Is your concern sort of that there's like too much baggage or too much like. 00:26:36.870 --> 00:26:41.040 Ego or, um, or just like maybe the implementation won't be what we want, or 00:26:41.330 --> 00:26:43.490 >> I would be afraid of baggage. 00:26:43.520 --> 00:26:49.070 Like we have so many things as bad as the type level programming situation is now. 00:26:49.370 --> 00:26:55.490 Um, people are at least familiar with it, you know, it's close at hand, uh, 00:26:55.500 --> 00:26:58.070 to continue borrowing rich Hickey isms. 00:26:58.580 --> 00:27:02.720 Um, and if we say, okay, well, all that is gone now and it's replaced 00:27:02.720 --> 00:27:04.160 with this thing that is better. 00:27:04.695 --> 00:27:06.254 But you have to relearn everything. 00:27:06.345 --> 00:27:09.495 Maybe that'll be too much and people will give up or maybe 00:27:09.495 --> 00:27:11.865 it'll be great and everyone will jump ship to, but I don't know, 00:27:12.334 --> 00:27:15.965 >> the, the, the like dream of dependent types is that 00:27:15.965 --> 00:27:17.345 they work just like values. 00:27:17.405 --> 00:27:18.635 And so there is nothing to learn. 00:27:19.054 --> 00:27:19.264 Right. 00:27:19.264 --> 00:27:19.534 >> Right. 00:27:21.185 --> 00:27:24.395 If you're already familiar with like the singletons library or like servant 00:27:24.395 --> 00:27:28.685 would have to be, I assume, completely rewritten and you know, maybe the 00:27:29.405 --> 00:27:32.165 >> Servant's and amazing piece of engineering, but I wish it didn't exist. 00:27:32.475 --> 00:27:34.185 >> Yeah, I think I agree with you. 00:27:34.245 --> 00:27:36.885 I really enjoy using it and everything that it gets us, but. 00:27:37.229 --> 00:27:37.560 Uh, 00:27:37.590 --> 00:27:38.820 >> it's beautiful when it works well. 00:27:38.820 --> 00:27:41.969 And when it doesn't you get these like type tornadoes, like five 00:27:41.969 --> 00:27:44.729 pages and they just scroll all the way across several times. 00:27:45.120 --> 00:27:45.419 Yeah. 00:27:45.860 --> 00:27:47.570 >> People like to give JavaScript a hard time for 00:27:47.570 --> 00:27:49.070 like the nested callback thing. 00:27:49.070 --> 00:27:51.489 But yeah, those servant type errors are, are much. 00:27:52.070 --> 00:27:53.539 >> It's amazing when it works. 00:27:53.539 --> 00:27:54.799 It's so fantastic. 00:27:54.860 --> 00:27:57.529 Um, and if you can follow the happy path, it's great. 00:27:57.889 --> 00:28:01.100 Unfortunately, I find I'm not good at following the happy path often. 00:28:01.189 --> 00:28:01.279 >> Yeah. 00:28:01.699 --> 00:28:02.689 We try to stay on it. 00:28:03.019 --> 00:28:04.909 Uh, I heard someone, I wish I could remember who, but I 00:28:04.909 --> 00:28:06.110 heard them say that like the. 00:28:06.524 --> 00:28:10.065 The best thing to do as a programmer is just, don't do weird stuff. 00:28:10.125 --> 00:28:12.795 And the hard part is figuring out what the weird stuff is. 00:28:12.885 --> 00:28:15.585 So yeah, with servants, as long as you stay on the straight and 00:28:15.585 --> 00:28:16.575 narrow, then it works great. 00:28:16.575 --> 00:28:17.264 But otherwise, yeah. 00:28:21.245 --> 00:28:25.295 Um, but yeah, I don't think we're going to get to the answer today of is dependently 00:28:25.295 --> 00:28:29.254 type task we're going to work or not, but I I'm just, um, I feel like if there's 00:28:29.254 --> 00:28:34.205 enough work involved with the switchover, then it's going to be a hard sell versus. 00:28:34.710 --> 00:28:36.960 Oh, well, I'll switch to Idris or I'll switch to, you 00:28:36.960 --> 00:28:38.160 know, whatever other language. 00:28:38.570 --> 00:28:39.050 >> Yeah. 00:28:39.170 --> 00:28:44.330 Haskell has the advantage in that we have users, all these other languages 00:28:44.330 --> 00:28:48.590 are really cool, but nobody, nobody really outside of the core group of 00:28:48.590 --> 00:28:52.640 researchers and like some academics as far as I can tell, really use these things. 00:28:52.670 --> 00:28:52.970 >> Right. 00:28:53.480 --> 00:28:57.170 >> Um, and so I think it would be hard to, I think Haskell has momentum. 00:28:57.170 --> 00:29:01.250 I think it's probably past the, the, I think it will exist forever. 00:29:01.800 --> 00:29:02.159 >> Right. 00:29:02.760 --> 00:29:03.420 Um, in one way 00:29:03.450 --> 00:29:04.500 >> in one way or another. 00:29:04.500 --> 00:29:04.740 Right. 00:29:04.800 --> 00:29:10.649 Um, so I, I think that's promising and, um, I'm really curious to see 00:29:10.649 --> 00:29:14.700 how they deprecate the old stuff for when dependent type Haskell happens. 00:29:14.700 --> 00:29:15.030 Right? 00:29:15.330 --> 00:29:15.570 >> Yeah. 00:29:15.629 --> 00:29:17.879 >> Do you still support all the weird type family stuff? 00:29:19.050 --> 00:29:22.340 I guess you have to, but I think it's weird semantic that's right. 00:29:22.430 --> 00:29:23.060 >> Yeah. 00:29:23.330 --> 00:29:29.130 I mean, given how GHC in particular support stuff now, um, It seems like 00:29:29.160 --> 00:29:30.690 they would support it for quite a while. 00:29:30.690 --> 00:29:31.020 You know, 00:29:31.410 --> 00:29:34.080 >> that's a very good point that that actually scares me more than 00:29:36.280 --> 00:29:39.450 >> GHC seems to be very, um, and, and probably for the best, but they 00:29:39.450 --> 00:29:42.780 seem to be very hesitant to deprecate anything and get rid of anything. 00:29:43.190 --> 00:29:47.510 >> I mean, it's, it's, it's amazing if you're a user of GHC, it's less. 00:29:47.510 --> 00:29:49.820 So if you are like a revolutionary. 00:29:50.145 --> 00:29:55.095 And I want to change the language so I understand why they do it, but I wish 00:29:55.095 --> 00:30:00.195 they wouldn't, but I don't, you know, if it weren't there, I would miss it, 00:30:00.195 --> 00:30:01.215 I guess, is what I'm trying to say. 00:30:01.545 --> 00:30:01.755 >> Right. 00:30:03.255 --> 00:30:03.525 Yeah. 00:30:04.055 --> 00:30:05.135 Um, so yeah. 00:30:05.195 --> 00:30:08.575 Uh, thanks for explaining, thinking with types to us, it sounds like both 00:30:08.575 --> 00:30:11.525 Cam and I could do well to read it and maybe, uh, understand what we're 00:30:11.525 --> 00:30:12.625 doing with servant a little better. 00:30:13.110 --> 00:30:13.350 Um, 00:30:13.409 --> 00:30:15.689 >> I think it would probably help if, uh, if you're just sort of 00:30:15.689 --> 00:30:18.360 bashing your head against the wall, why doesn't, why doesn't this work. 00:30:18.419 --> 00:30:21.110 Whereas, and, 00:30:22.040 --> 00:30:25.610 >> um, but yeah, I'd like to, uh, shift gears a little bit and talk about 00:30:25.610 --> 00:30:31.040 your polysemy library, um, which maybe is a little old hat by now, but, um, yeah. 00:30:31.100 --> 00:30:31.759 Tell us about it. 00:30:31.759 --> 00:30:33.499 What is it why people may want to use it? 00:30:34.394 --> 00:30:35.144 >> Yeah. 00:30:35.235 --> 00:30:38.024 Um, so polysemy is free. 00:30:38.024 --> 00:30:42.034 Monads, um, done better, I guess is how I would phrase it. 00:30:42.304 --> 00:30:42.695 >> Okay. 00:30:42.784 --> 00:30:47.314 >> Um, and so the idea is sort of, you can abstract away from a specific monad 00:30:47.314 --> 00:30:49.534 stack, uh, like a monad transformer thing. 00:30:50.104 --> 00:30:54.064 And instead you can say, ah, I have these effects in scope and these 00:30:54.064 --> 00:30:55.894 effects can be like really fine tuning. 00:30:55.894 --> 00:30:58.445 Cause they like, I have a connection to an FTP client. 00:30:58.935 --> 00:31:03.195 Perfect a FTP server, or I have like, um, I have the ability to 00:31:03.195 --> 00:31:04.784 read and write to some data source. 00:31:05.024 --> 00:31:08.955 That is a key value source state fully, but I don't care what that is. 00:31:08.955 --> 00:31:10.874 Maybe that's uh, uh, yeah, so. 00:31:11.939 --> 00:31:15.090 Um, so the idea is sort of, you can separate your business logic, 00:31:15.360 --> 00:31:18.120 which is I have some abstractions I care about from the actual 00:31:18.120 --> 00:31:19.439 implementations of those things. 00:31:20.549 --> 00:31:25.919 Um, that's the sell at the high level, and I guess of all of all effects 00:31:25.919 --> 00:31:30.959 systems and, uh, and then later you can choose how to interpret those systems. 00:31:30.989 --> 00:31:33.749 And so I can say, Oh, I have this, this key value store. 00:31:33.749 --> 00:31:37.709 And like maybe that's Redis or maybe that is HTTP requests. 00:31:38.070 --> 00:31:39.629 Or maybe it's a local file, right. 00:31:39.629 --> 00:31:43.440 Or maybe it's just a local state monad, um, it, the, the 00:31:43.440 --> 00:31:44.820 application shouldn't care. 00:31:45.600 --> 00:31:45.960 >> Right. 00:31:46.440 --> 00:31:48.420 You only care about the interface that it exposes. 00:31:48.450 --> 00:31:49.200 >> Yeah, exactly. 00:31:49.200 --> 00:31:51.960 Like, and so, so the pitch is sort of like, what did the 00:31:51.960 --> 00:31:53.129 business people care about? 00:31:53.160 --> 00:31:55.160 Can we express them in 10 lines of code? 00:31:55.610 --> 00:31:55.910 Right. 00:31:56.510 --> 00:31:59.420 And generally if you're at a high enough, high enough level of 00:31:59.420 --> 00:32:00.680 abstraction, the answer is yes. 00:32:01.550 --> 00:32:03.080 Um, and, and that's really lovely. 00:32:03.080 --> 00:32:03.290 Right. 00:32:03.290 --> 00:32:06.139 But when you get to a point where all of your business logic. 00:32:06.690 --> 00:32:07.919 Is comprehensible. 00:32:07.980 --> 00:32:12.510 And then you sort of transform it through these transformations of, I 00:32:12.510 --> 00:32:16.980 have this one effect I can implement it either directly, or I can say I can 00:32:16.980 --> 00:32:18.510 implement it in terms of other effects. 00:32:18.690 --> 00:32:22.290 And so I can say, I can implement this state, but only if I've 00:32:22.290 --> 00:32:23.850 got access to a web client. 00:32:24.940 --> 00:32:25.200 Right. 00:32:25.620 --> 00:32:28.350 Um, but then that web client, you might also want to mock. 00:32:28.620 --> 00:32:31.020 And so it's not actually talking to the web, right. 00:32:31.574 --> 00:32:31.874 >> Right. 00:32:31.904 --> 00:32:36.225 >> Uh, so, so that's sort of the, the idea, um, polysemy, what it brings 00:32:36.225 --> 00:32:39.614 to the table is makes it much easier to do these sorts of things, um, 00:32:40.235 --> 00:32:41.134 >> easier than what 00:32:41.824 --> 00:32:47.205 >> easier than, uh, there's another library called like freer-simple 00:32:47.254 --> 00:32:49.654 and freer-effects and freer. 00:32:49.864 --> 00:32:53.314 And, uh, there's like 20 different free monad libraries in various 00:32:53.314 --> 00:32:56.044 States of, uh, love really. 00:32:58.739 --> 00:33:03.419 Um, and the idea for this was I wanted it to be, um, easy and 00:33:03.419 --> 00:33:06.269 fast and give good error messages. 00:33:06.269 --> 00:33:07.229 If you screwed something up. 00:33:08.220 --> 00:33:09.899 And so that those were the goals. 00:33:09.929 --> 00:33:13.409 And, um, the last one in particular was quite challenging. 00:33:13.470 --> 00:33:18.240 Uh, it requires like it requires a plugin to run, which in 00:33:18.240 --> 00:33:19.590 retrospect was a bad idea. 00:33:20.129 --> 00:33:22.409 Um, cause it means that you just have to keep that up to date 00:33:22.409 --> 00:33:25.320 with GHC versions in a way that like a library doesn't need to be 00:33:25.649 --> 00:33:25.980 >> right. 00:33:26.720 --> 00:33:26.899 Wait. 00:33:26.899 --> 00:33:30.830 So it, it requires a plugin in order to work at all or in order to get down there? 00:33:30.980 --> 00:33:34.040 >> No, not in order to work at all, but in order to, um, to 00:33:34.040 --> 00:33:35.689 like get type inference working. 00:33:35.840 --> 00:33:36.080 Hmm. 00:33:36.495 --> 00:33:36.675 Okay. 00:33:36.705 --> 00:33:40.435 There's a lot of programs you'll write in polysemy that without the plugin, 00:33:40.605 --> 00:33:42.825 you'll say, obviously this is what I want. 00:33:42.825 --> 00:33:44.865 And it's like, Whoa, I don't know what this effect is. 00:33:44.865 --> 00:33:46.034 And be like, there's only one effects. 00:33:46.034 --> 00:33:49.335 There is clearly that one, but it doesn't know. 00:33:49.335 --> 00:33:52.455 And so there's a, there's a plugin that like solves those. 00:33:52.455 --> 00:33:54.975 So it's sort of a type checker addition. 00:33:55.595 --> 00:33:55.955 >> Cool. 00:33:56.405 --> 00:33:56.735 >> Yeah. 00:33:57.274 --> 00:33:59.855 >> Um, but yeah, I, uh, I can appreciate that. 00:34:00.285 --> 00:34:03.375 Keeping up with the GFC API is a little tedious. 00:34:03.435 --> 00:34:05.655 Um, we were just talking about how good they are at maintaining 00:34:05.655 --> 00:34:06.614 backwards compatibility. 00:34:06.645 --> 00:34:09.614 That's for their, you know, the compiler and everything. 00:34:09.915 --> 00:34:12.605 Not for the internals, which shift around much more often. 00:34:13.025 --> 00:34:13.355 >> Right. 00:34:13.625 --> 00:34:15.935 Um, on the, on the other hand, like I appreciate it. 00:34:15.935 --> 00:34:20.014 I wish there were a better compatibility story though. 00:34:20.195 --> 00:34:25.085 There's like the GHC lib now, uh, which I think solves this problem. 00:34:25.415 --> 00:34:26.554 I've never really worked against. 00:34:26.554 --> 00:34:27.514 I think it's newer than. 00:34:28.019 --> 00:34:28.949 My issues, but 00:34:28.979 --> 00:34:32.580 >> yeah, there's the GHC library for like parsing, right. 00:34:32.850 --> 00:34:36.179 That, uh, Shayne Fletcher, I think maintains. 00:34:36.629 --> 00:34:39.899 Um, and yeah, that seems really nice to say like, okay, I don't really 00:34:39.899 --> 00:34:43.709 use all the particulars or I can do a, uh, pretty straightforward 00:34:43.709 --> 00:34:44.850 mapping between all the versions. 00:34:44.850 --> 00:34:45.779 And he has done that for you. 00:34:46.609 --> 00:34:50.299 >> That one, unfortunately doesn't work if you also need GHC the library. 00:34:50.449 --> 00:34:50.749 >> Right. 00:34:51.319 --> 00:34:54.859 >> Um, because, uh, the parser has just redefined all the types of needs. 00:34:55.475 --> 00:34:59.235 Which is lovely, except when you now want to talk back to GHC it's like, Oh, 00:34:59.265 --> 00:35:01.995 my expression is not the same as your expression, even though it's identical. 00:35:02.285 --> 00:35:03.005 Oh, great. 00:35:03.305 --> 00:35:04.115 >> That's unfortunate. 00:35:04.115 --> 00:35:04.415 Yeah. 00:35:04.625 --> 00:35:04.925 >> Yeah. 00:35:04.955 --> 00:35:05.765 So, um, okay. 00:35:06.025 --> 00:35:08.945 I think it's, it's a much better state of affairs than the old like 00:35:08.945 --> 00:35:11.105 source extensions situation was. 00:35:11.525 --> 00:35:13.985 Um, but I haven't had the joy of working with it yet. 00:35:15.065 --> 00:35:15.365 >> Yeah. 00:35:15.395 --> 00:35:20.835 Um, Uh, I will say that it's nice to have the option of writing these plugins, you 00:35:20.835 --> 00:35:26.415 know, and I think that, uh, there are a couple kind of big name ones, I guess I 00:35:26.415 --> 00:35:29.265 can only really think of one, the record dot pre-processor has kind of like a 00:35:29.265 --> 00:35:31.365 preview of language extensions to come. 00:35:31.725 --> 00:35:35.115 Um, but interesting to see them used here for an effect library as well. 00:35:35.855 --> 00:35:36.335 >> Yeah. 00:35:36.485 --> 00:35:41.115 Um, I think these days, I don't really endorse free monads. 00:35:41.595 --> 00:35:42.045 >> Okay. 00:35:42.825 --> 00:35:45.975 >> Alexis, Alexis King wrote an article maybe this 00:35:45.975 --> 00:35:46.785 year or maybe last year. 00:35:46.845 --> 00:35:47.655 It's hard to keep track 00:35:49.425 --> 00:35:50.355 >> time as a flat circle. 00:35:50.355 --> 00:35:50.865 Yeah, it's weird. 00:35:50.865 --> 00:35:51.134 >> Yes. 00:35:51.585 --> 00:35:58.275 I'm talking about how all of my claims for performance were untrue and, um, 00:35:59.085 --> 00:36:00.675 She was absolutely right about that. 00:36:00.705 --> 00:36:02.775 And unintentionally, unintentionally untrue. 00:36:02.985 --> 00:36:03.215 Right. 00:36:03.215 --> 00:36:06.885 And I wasn't going out of my way to lie about it, but, um, some issues 00:36:06.885 --> 00:36:09.915 sort of in the benchmarking and how the simplifier works and just like, there 00:36:09.915 --> 00:36:15.225 were several systematic errors that led to my performance claims being untrue. 00:36:15.645 --> 00:36:17.205 Um, so that was part of it. 00:36:17.235 --> 00:36:21.105 And then, um, The good news, I guess, or bad news, depending on how you 00:36:21.105 --> 00:36:24.435 look at it, as it sort of all effect systems have terrible performance, 00:36:24.435 --> 00:36:28.875 including MTL, and nobody noticed because everybody's bad at benchmarking. 00:36:30.964 --> 00:36:32.015 >> It's a hard thing to do. 00:36:32.404 --> 00:36:32.585 >> Yeah. 00:36:32.615 --> 00:36:32.855 >> Yeah. 00:36:32.855 --> 00:36:37.714 It's not to say like, MTL is as bad as puts to me, but, um, so on one hand, like 00:36:37.714 --> 00:36:40.235 I claimed the performance doesn't really matter for most of the things we write. 00:36:40.800 --> 00:36:41.009 Right. 00:36:41.009 --> 00:36:43.740 Most of the time you're waiting on a network call or, or, 00:36:44.160 --> 00:36:45.060 you know, IO or something. 00:36:45.060 --> 00:36:47.790 So usually it doesn't matter, but it's, it would still be nice to get that. 00:36:47.790 --> 00:36:48.090 Right. 00:36:48.690 --> 00:36:53.670 Um, and on the other hand, um, the thing is I realized, I think 00:36:53.700 --> 00:36:57.270 we're all better off just sort of mock, like writing pure programs. 00:36:58.170 --> 00:37:01.890 If you just push all the effects as far out as possible, that's 00:37:01.890 --> 00:37:03.540 just a better solution in general. 00:37:03.855 --> 00:37:04.215 >> Yeah. 00:37:04.365 --> 00:37:05.515 Um, are you familiar with, 00:37:05.515 --> 00:37:08.235 >> Matt parsons actually has a lot of like good articles on how to do this 00:37:08.295 --> 00:37:08.625 >> right now? 00:37:09.215 --> 00:37:10.965 The three layer Haskell cake, I think is one, 00:37:10.965 --> 00:37:15.255 >> um, that one I'm not as Fonda, he's got one called invert. 00:37:15.255 --> 00:37:15.915 Your mocks. 00:37:16.095 --> 00:37:16.485 >> There you go. 00:37:16.545 --> 00:37:19.155 >> And that one is sort of all about how to like pull out 00:37:19.305 --> 00:37:21.625 the pure parts of effective programs and I really endorse that 00:37:22.505 --> 00:37:22.745 >> yeah. 00:37:22.775 --> 00:37:28.295 And I think, uh, there's some, I I'm drawn to that, uh, approach 00:37:28.295 --> 00:37:32.105 of designing software because it extends outside of Haskell as well. 00:37:32.430 --> 00:37:34.620 Uh, if you're familiar with Gary Bernhardt, he has a talk 00:37:34.620 --> 00:37:36.930 about, um, uh, what is it? 00:37:37.799 --> 00:37:39.899 Imperative shell, pure core. 00:37:40.140 --> 00:37:41.850 That may not be the exact wording, but like yeah. 00:37:41.879 --> 00:37:43.319 Push everything to the outside. 00:37:43.319 --> 00:37:46.049 And then on the inside, you've already done all the network, 00:37:46.049 --> 00:37:47.250 all the database, all that. 00:37:47.250 --> 00:37:48.600 And you just deal with the pure stuff. 00:37:49.350 --> 00:37:52.319 >> Unfortunately, humans seem bad at writing code like that, especially 00:37:52.319 --> 00:37:55.740 when like time pressure arises and it's like, Oh, I just need IO here. 00:37:56.490 --> 00:37:57.810 I can't be fucked to do it the right way. 00:37:57.810 --> 00:37:58.049 Right. 00:37:58.680 --> 00:38:02.460 Um, and then over time that stuff accumulates and sort of, I think that 00:38:02.460 --> 00:38:06.629 was really what I was rallying against with polysemy was, um, I had worked 00:38:06.629 --> 00:38:10.830 in like a pretty atrocious code base professionally, which just the entire 00:38:10.830 --> 00:38:13.200 thing was in IO and there was no. 00:38:14.019 --> 00:38:17.700 Sort of, um, discipline anywhere about what things were pure and so just 00:38:19.109 --> 00:38:23.189 like we, we found a multi-million dollar bug that bit us, because 00:38:23.189 --> 00:38:24.269 we just couldn't test anything. 00:38:24.269 --> 00:38:25.140 Cause it was all in IO. 00:38:25.970 --> 00:38:26.539 >> Yikes. 00:38:26.809 --> 00:38:27.379 That's pretty bad. 00:38:27.379 --> 00:38:29.120 So I can see why that would motivate you. 00:38:29.720 --> 00:38:30.169 >> Yeah. 00:38:30.419 --> 00:38:32.209 The problem is sort of motivation. 00:38:32.209 --> 00:38:34.669 Like these are, it's only ever after the fact, right? 00:38:34.759 --> 00:38:34.970 >> Yeah. 00:38:35.355 --> 00:38:36.225 >> Nobody really cares. 00:38:36.225 --> 00:38:38.985 If you say, Hey, everything's an IO and it's going to cause 00:38:38.985 --> 00:38:42.645 us millions of dollars, but it doesn't work until it happens. 00:38:42.645 --> 00:38:42.915 Right. 00:38:42.915 --> 00:38:43.155 So 00:38:43.185 --> 00:38:43.455 >> right. 00:38:43.835 --> 00:38:47.075 And then when it happens, you get the, uh, the peanut gallery on 00:38:47.075 --> 00:38:49.445 Reddit saying like, ah, you could could've, you could caught this. 00:38:50.585 --> 00:38:51.095 >> Exactly. 00:38:51.155 --> 00:38:51.545 Yeah. 00:38:52.085 --> 00:38:56.555 Um, so yeah, so I think it was, um, it was a really interesting project for me to 00:38:56.555 --> 00:39:00.605 just go through and learn how to do all of this stuff and really flex my type level. 00:39:01.005 --> 00:39:01.575 muscles. 00:39:01.860 --> 00:39:02.190 >> Yeah. 00:39:02.460 --> 00:39:04.230 You can say lots of type of programming in there. 00:39:04.760 --> 00:39:05.660 >> Yeah, exactly. 00:39:05.720 --> 00:39:10.730 Um, and I'm happy that it's taken off, um, in a way that I didn't expect. 00:39:10.760 --> 00:39:16.070 Um, I think that's exciting to me and also a little scary. 00:39:18.590 --> 00:39:20.810 >> It's scary how people are using yourself. 00:39:21.800 --> 00:39:25.430 >> No, because how I would like to write programs anymore. 00:39:25.760 --> 00:39:29.030 I think I've, I've learned something now that I hadn't learned back then. 00:39:29.030 --> 00:39:29.510 And so. 00:39:30.180 --> 00:39:36.380 People using that sort of reflects like either I'm wrong now or right. 00:39:36.910 --> 00:39:38.750 >> And neither of which is a good place to be. 00:39:38.810 --> 00:39:39.620 >> Yeah, exactly. 00:39:39.650 --> 00:39:42.980 And so I'm not sure what the answer is, but, um, anyway, 00:39:43.009 --> 00:39:44.450 so I'm happy people use it. 00:39:44.690 --> 00:39:46.009 I'm happy I get the credit for it. 00:39:46.549 --> 00:39:50.900 Uh, and you know, there's worse things in the world than people using your software. 00:39:51.110 --> 00:39:51.500 >> Yeah. 00:39:51.950 --> 00:39:54.470 Uh, I'm I'm curious, we were talking earlier about, uh, 00:39:54.500 --> 00:39:56.630 dependently typed programs and how. 00:39:56.970 --> 00:39:59.490 You know, Haskell is kind of halfway there and it's awkward. 00:39:59.939 --> 00:40:04.529 Um, I have a passing familiarity with pure script, which has sort of an effect 00:40:04.540 --> 00:40:06.540 system baked in thanks to the row types. 00:40:06.899 --> 00:40:09.990 Uh, um, do you have any experience with that and how does it kind of 00:40:09.990 --> 00:40:11.509 stack up against the free monads? 00:40:12.109 --> 00:40:14.450 >> I don't have really any experience with that. 00:40:14.540 --> 00:40:15.649 I didn't know it existed. 00:40:15.830 --> 00:40:17.540 And then they sort of chopped out of IO. 00:40:18.044 --> 00:40:18.435 Yeah. 00:40:18.444 --> 00:40:19.305 Kept the row types. 00:40:19.305 --> 00:40:20.895 And I don't, I don't know anything more than that. 00:40:21.165 --> 00:40:21.495 >> Yeah. 00:40:21.995 --> 00:40:24.935 Um, again, I only have a passing familiarity, so apologies 00:40:24.935 --> 00:40:27.064 to anyone in the pure script community if I get this way wrong. 00:40:27.095 --> 00:40:32.375 But, uh, from what I recall, they had, um, or they have row types, uh, so 00:40:32.375 --> 00:40:35.944 they can do like anonymous records and those also exist at the type level. 00:40:35.944 --> 00:40:36.725 So you can have. 00:40:37.335 --> 00:40:41.595 And anonymous, uh, map of named things too. 00:40:41.865 --> 00:40:43.545 Uh, I think they just called them effects. 00:40:43.545 --> 00:40:45.945 So you'd have like some kind that represented. 00:40:45.945 --> 00:40:49.425 I can talk to the database and your function and say, okay, I 00:40:49.425 --> 00:40:50.685 need this effect in order to work. 00:40:50.745 --> 00:40:54.135 And I think they don't do that anymore. 00:40:54.165 --> 00:40:57.375 You can, if you want to, but like officially they effectively 00:40:57.375 --> 00:40:59.805 just have IO as their effect. 00:41:00.195 --> 00:41:04.035 Um, so it was, uh, interesting for me to see like, okay, they have all 00:41:04.035 --> 00:41:06.255 this power, they can express all this stuff at the type level and. 00:41:06.765 --> 00:41:09.645 They kind of don't want to, um, and they'll go back to doing things 00:41:09.645 --> 00:41:10.455 the way that Haskell does it. 00:41:10.935 --> 00:41:11.115 >> Yeah. 00:41:11.675 --> 00:41:12.965 I don't know why. 00:41:13.055 --> 00:41:15.785 I didn't maybe, maybe they've tried it and given it a go and 00:41:15.785 --> 00:41:17.075 realized, Oh, it doesn't work. 00:41:17.525 --> 00:41:22.145 Um, maybe just like Haskell has the prestige and there's this 00:41:22.145 --> 00:41:24.915 weird monad thing where once you realize, once you learn about 00:41:24.915 --> 00:41:26.045 monads, you need to write about them. 00:41:26.504 --> 00:41:26.754 >> Yeah. 00:41:26.754 --> 00:41:30.165 >> And like, I, I think that is a big problem. 00:41:30.395 --> 00:41:32.794 I don't know if that's relevant here, but I think I could see that 00:41:32.794 --> 00:41:35.524 happening where like someone says, Oh, monad transformers let's use 00:41:35.524 --> 00:41:36.904 those because Haskell uses those. 00:41:37.865 --> 00:41:40.065 Um, again, I don't know anything about pure scripts. 00:41:40.084 --> 00:41:42.095 I don't know if that's the sentiment they have, but, um, 00:41:42.455 --> 00:41:45.964 >> so, uh, to try to shove these pieces together, I think one of the 00:41:45.964 --> 00:41:52.785 problems that PureScript ran into was that, um, if your effect kind like the 00:41:52.785 --> 00:41:55.605 thing that says, Hey, I need to be able to talk to, or write to the console 00:41:55.605 --> 00:42:00.915 or read from it or whatever, if that isn't shared among every library that 00:42:00.915 --> 00:42:04.725 you're working with, then you get this very strange fracturing where you have, 00:42:04.725 --> 00:42:09.165 let's say two different Redis libraries and they each define their own effect. 00:42:09.465 --> 00:42:13.515 And so if you have one and you want to use the other, suddenly you have to like redo 00:42:13.515 --> 00:42:17.265 all of the effects all the way up your chain, because you have both of them now. 00:42:17.759 --> 00:42:21.839 Um, and I, I feel like Haskell also can have this problem where like, 00:42:21.870 --> 00:42:22.559 >> absolutely we do, 00:42:22.559 --> 00:42:25.799 >> you know, if some fundamental type isn't defined low enough, then everybody 00:42:25.799 --> 00:42:27.600 defines their own and it becomes a zoo. 00:42:28.140 --> 00:42:32.009 Um, and maybe that's just way more annoying to deal with when 00:42:32.009 --> 00:42:33.419 you're at the effect level. 00:42:34.370 --> 00:42:35.509 >> I think that's true. 00:42:35.600 --> 00:42:39.470 Um, I'm hoping that people don't, I guess that's one of the things 00:42:39.479 --> 00:42:42.289 I liked about polysemy it was sort of the high level idea of like, 00:42:42.410 --> 00:42:43.609 I just have some key value state. 00:42:44.430 --> 00:42:44.730 Right. 00:42:45.180 --> 00:42:48.570 Um, the thing about if you have like a Redis effect, is that the only 00:42:48.570 --> 00:42:49.980 implementation of that can be Redis 00:42:50.280 --> 00:42:50.580 >> right. 00:42:51.270 --> 00:42:55.260 >> There's you can't do anything other than like Redis or reimplementing Redis 00:42:57.170 --> 00:42:57.880 >> I mean, you could try. 00:42:58.430 --> 00:43:00.450 >> Yeah, I could try, but at that point, why right, 00:43:00.450 --> 00:43:00.800 >> right. 00:43:00.980 --> 00:43:01.880 >> Um, and so. 00:43:02.384 --> 00:43:05.475 I think there's a value in like, keeping your effects as 00:43:05.475 --> 00:43:06.915 small as possible exact exactly. 00:43:06.915 --> 00:43:10.575 For this reason, regardless of the system, or like, if it's just MTL or 00:43:10.575 --> 00:43:15.495 even if it's just like making a monad stack a concrete monad stack of just like 00:43:15.615 --> 00:43:20.715 keeping your effects as small as possible, because otherwise you're making choices 00:43:20.805 --> 00:43:22.395 that you're going to have to live with. 00:43:23.055 --> 00:43:23.445 Right. 00:43:23.985 --> 00:43:28.095 Um, and unfortunately, like you have to make choices at some point, but again, if 00:43:28.095 --> 00:43:30.015 you can push them as far out as possible, 00:43:30.645 --> 00:43:30.915 >> Yeah, 00:43:31.545 --> 00:43:33.105 >> that makes life easier. 00:43:33.195 --> 00:43:35.265 >> I agree with you, but I'm not surprised to hear you say that 00:43:35.265 --> 00:43:37.065 based on algebra driven design. 00:43:37.065 --> 00:43:41.955 Cause it's like, you know, if your interface is I am Redis, then it's 00:43:41.955 --> 00:43:44.715 really hard to come up with properties about that to mock it, to do anything. 00:43:44.715 --> 00:43:47.085 But if you're interface is,, I'm a key value store. 00:43:47.235 --> 00:43:47.805 Much easier. 00:43:48.165 --> 00:43:48.675 >> Exactly. 00:43:48.675 --> 00:43:48.945 Yeah. 00:43:49.505 --> 00:43:50.895 What are the properties of Redis? 00:43:52.835 --> 00:43:54.065 I don't know if there are any right. 00:43:54.655 --> 00:43:56.105 Guaranteed to get back what you put in. 00:43:56.675 --> 00:43:57.005 >> Yeah. 00:43:57.944 --> 00:43:58.475 Uh, yeah. 00:44:01.694 --> 00:44:04.875 Um, well, we've covered a lot of good topics here. 00:44:04.935 --> 00:44:08.145 Uh, Sandy, is there anything else, uh, you know, what are you working on? 00:44:08.145 --> 00:44:09.194 What are you looking forward to? 00:44:09.285 --> 00:44:10.095 Uh, what's next for you? 00:44:10.754 --> 00:44:14.705 >> Yeah, so right now I'm working like full-time on a Haskell wingman. 00:44:14.705 --> 00:44:18.904 Wingman for Haskell that branding is still being figured out, 00:44:18.904 --> 00:44:19.384 >> up in the air. 00:44:19.575 --> 00:44:19.765 >> Yeah. 00:44:19.765 --> 00:44:20.585 Yeah, exactly. 00:44:20.615 --> 00:44:24.004 Um, and so I'm trying to make that, like my full-time life. 00:44:24.794 --> 00:44:28.125 Um, and so I've got a Patrion for that if, uh, if anyone's interested 00:44:28.125 --> 00:44:29.955 in helping support me through that, 00:44:30.285 --> 00:44:30.615 >> for sure. 00:44:30.645 --> 00:44:33.435 Um, yeah, that's sort of linked to that in the show notes. 00:44:33.794 --> 00:44:34.214 >> Marvelous. 00:44:34.214 --> 00:44:34.544 Thank you. 00:44:34.995 --> 00:44:36.855 Um, that's like where all my time's going. 00:44:36.855 --> 00:44:38.714 I'm putting like 10 hours a day into it right now. 00:44:38.984 --> 00:44:39.225 >> Wow. 00:44:39.285 --> 00:44:43.814 >> And so, uh, yeah, besides that, um, I think that's it 00:44:43.814 --> 00:44:45.765 really like, that's all I'm doing. 00:44:46.395 --> 00:44:46.964 It feels good. 00:44:47.024 --> 00:44:47.504 Honestly. 00:44:47.924 --> 00:44:49.725 It's nice to have like a project you really care about. 00:44:49.984 --> 00:44:50.345 >> Yeah. 00:44:50.555 --> 00:44:53.524 And if people want to find you online, where should they go look for you? 00:44:54.194 --> 00:44:59.084 >> Yeah, I'm, uh, I'm online at reasonablypolymorphic.com is my math blog. 00:44:59.084 --> 00:45:02.654 And I also have sandymaguire.me, which is my personal blog. 00:45:02.895 --> 00:45:05.595 And it turns out like, I'm, I'm going to shill them both, but 00:45:05.805 --> 00:45:08.834 there's really no market for like, there's no intersection of people 00:45:08.834 --> 00:45:09.975 who care about both of those things. 00:45:11.055 --> 00:45:14.415 People care about my math stuff, or they care about like me as a person, 00:45:14.444 --> 00:45:16.845 but I learned that the hard way. 00:45:16.845 --> 00:45:19.035 And you just split them up, but I'll shill them both. 00:45:19.634 --> 00:45:23.024 And, uh, I think that's, that's pretty much all my online presence. 00:45:23.955 --> 00:45:24.435 >> All right. 00:45:25.275 --> 00:45:26.115 Well, yeah. 00:45:26.145 --> 00:45:28.725 Thank you so much for being on the show with us today. 00:45:28.755 --> 00:45:29.985 It's been great to have you here. 00:45:30.395 --> 00:45:31.085 >> Oh my pleasure. 00:45:31.115 --> 00:45:31.775 Thanks for having me. 00:45:31.775 --> 00:45:34.205 And I just want to thank you both for like all the great things 00:45:34.205 --> 00:45:35.345 you've been doing for the community. 00:45:35.675 --> 00:45:36.155 >> Thanks. 00:45:36.245 --> 00:45:36.875 I appreciate it. 00:45:36.875 --> 00:45:39.209 >> Gonna we keep on keeping on. 00:45:39.539 --> 00:45:39.809 >> Yeah. 00:45:39.839 --> 00:45:40.289 >> I like that. 00:45:40.319 --> 00:45:42.569 Cheers, please do. 00:45:43.160 --> 00:45:46.609 >> Uh, and, uh, thank you to the listeners of the Haskell weekly podcast. 00:45:46.640 --> 00:45:49.160 Um, thanks for tuning in, even though we're not here every 00:45:49.160 --> 00:45:50.419 week, we're here most weeks. 00:45:50.939 --> 00:45:55.950 Uh, Uh, I've been your host Taylor Fausak and our special guest 00:45:55.950 --> 00:45:57.660 this week was Sandy Maguire. 00:45:57.720 --> 00:46:00.109 Also with me today was Cameron Gera. 00:46:00.690 --> 00:46:03.839 If you want to find out more about Haskell weekly, you can visit our 00:46:03.839 --> 00:46:06.160 website, which is HaskellWeekly.News. 00:46:06.830 --> 00:46:11.150 If you like the show, please rate and review us on Apple podcasts. 00:46:11.210 --> 00:46:14.029 Uh, and if you have any feedback, you can tweet it at us. 00:46:14.339 --> 00:46:16.640 Our handle is @HaskellWeekly. 00:46:17.339 --> 00:46:20.640 Um, and yeah, we're elsewhere on the web, but those are the main ones. 00:46:21.390 --> 00:46:21.629 >> Yep. 00:46:21.899 --> 00:46:22.620 And Haskell weekly. 00:46:22.620 --> 00:46:22.680 Yeah. 00:46:22.789 --> 00:46:27.499 Brought to you by ITProTV, an ACI learning company and our employer. 00:46:27.859 --> 00:46:32.299 They would like to offer you 30% off your subscription by using promo 00:46:32.299 --> 00:46:35.390 code HaskellWeekly30 at checkout. 00:46:35.809 --> 00:46:40.995 Um, so if you're ever interested in it, cybersecurity training, Yeah, we 00:46:40.995 --> 00:46:42.884 have anything and everything you need. 00:46:42.884 --> 00:46:46.095 So check it out if you're interested, but I think that about 00:46:46.125 --> 00:46:48.015 does it for us Taylor and Sandy. 00:46:48.765 --> 00:46:49.935 >> Yeah, sure. 00:46:49.935 --> 00:46:50.174 It does. 00:46:50.174 --> 00:46:52.875 So thanks for joining us and we'll see you next week.