Haskell Weekly

>> hello and welcome to the Haskell weekly podcast. This is a show about Haskell a purely functional programming language. I'm your host, Cameron Gera, an engineer here at ITProTV. And with me today is Taylor Fausak. One of the engineers on my team and my boss. Thanks for joining me today, Taylor.

>> Yeah, I'm happy to be here, cam, and I'm really excited today because we have a special guest with us, Sandy McGuire. Thanks for joining us, Sandy.

>> Thanks for having me guys. I'm excited to be here.

>> Yeah, this is awesome. So Sandy, for people who may not know who you are already, how would you describe yourself?

>> Uh, I write a lot of Haskell.

>> Good start.

>> Yeah. I don't know. You caught me off guard here, Taylor.

>> Well, uh, then let me say some things that I know about you, so

>> you're better prepared than I am here.

>> In addition to writing a lot of Haskell, you write a lot of Haskell content. You've authored two books, uh, thinking with types and algebra driven design. Uh, neither of which I think are necessarily like Haskell books, quote unquote, but they do sort of intersect quite a bit.

>> Yeah, I think that's very fair.

>> And, uh, you also author the blog reasonably polymorphic. And, uh, you're the author of the polysemy am I saying that, right?

>> Yeah.

>> Polysemy library for, uh, what's that like freer effects effect system.

>> Yeah. Some sort of weird effect system.

>> Uh, and more recently you've been working on wing man for Haskell, which is a tool for, I would say program synthesis, maybe.

>> Yeah. That's a, that's a great description of it.

>> So you're telling me it's not. Like the apex weapon, the wing man, you know, is that it?

>> No, it's not. I really wanted to call it copilot, but that one's turned out to already be used.

>> Really?

>> Yeah.

>> What's called copilot

>> there's. Um, there's like a NASA DSL for doing like verified C plus plus programs or something. Not quite the same thing. No. Um, but it's a great name and I'm upset that they got it.

>> Well, wing man is good too. I like that.

>> Thank you.

>> Um, so maybe let's launch into that. Could you tell us a little about wingman? What does it do?

>> Sure. Um, so wingman is a plugin for the Haskell language server and the idea is it tries to automate away, um, the like ho hold driven design. Um, philosophy where you, you say, like, I don't really know the code I'm writing, I'm going to put it in a hole. And then the compiler tells you what that hole has type. Right. It gives you the type of it. And then you say, okay, well I know this thing has some type and I sort of know roughly what type I think it should be. So you, maybe you put an fmap in and then you put it in another hole and then it says, okay, well now the hole has changed because you've sort of synthesize some of the program. Um, and for a lot of code code, this turns out to like, Really what you're doing is just typing in the things GHC tells you to type.

>> Yeah.

>> Right.

>> And it's, it's a little silly, right. So I thought, why not? Why don't we just automate that? Right. Why don't we just automate that conversation with the compiler and see if we can synthesize all sorts of the dumb programs that you would write yourself if you just follow the holes.

>> Yeah. Uh, we do that surprisingly often here. Uh, We haven't been able to get HLS to work reliably on our code base, unfortunately, but we do the, like put a typed hole in there and then copy paste or just type in whatever GHC suggests. If there's only one thing often there are multiple, you know, and then you pick the right one, the one that's probably not, mempty.

>> It always suggests unsafe coerce.

>> Yeah.

>> Wingman doesn't do that, thankfully.

>> The trick is to not have that one in scope, I think. But yeah, we get mempty a lot or like const or something like that.

>> Yeah, absolutely.

>> Um, but yeah, it is kind of silly to be doing this copy pasting, and it sounds like wingman automates some of that, but also I got the impression that, that it does more than just naively filling in the whole, the GHC suggests is that right?

>> Um, yeah, so there, there's sort of two things there. One of which is, uh, we have this, this like proof search going on in the background. And so it's actually trying to find a good program, um, by, for some definition of good. Right. And that sort of usually if you write code, um, you'll. Often, if you like see code that a beginner is written, they'll like, it'll be crazy. And like the type signature doesn't really correspond to the definition. And it's sort of hard to put your hand on what that means. Um, but so, so like a good metric for that is sort of linearity. You want generally your variables to only be used once, right. A program where if you can synthesize a solution only uses your variables once that's usually better than one that uses the multiple times.

>> Right.

>> Or not at all right, exactly. Which is the const the unsafe course sort of solution. Um, so that is sort of the, the interesting part of it. Um, and then we also have a bunch of like ergonomic things going on. And so, um, Wingman, we'll also do things like case splitting. And so you can say, um, Hey, I want you to case split on X and that is some weird ADT and it'll, um, it'll like multiply out every match. So you'll get multiple definitions of the function for every possible constructor. Right. So that's, that turns like one typed hole into many potentially. Right. And then you keep on filling and from there it will. Yeah.

>> Hmm.

>> Cool. And you mentioned linearity, uh, I don't want to go too far off on a tangent here, but I'm wondering, is there with linear types landed in GHC nine? Is there an opportunity for wingman to make use of that information and say, okay, I know that this needs to be used, so therefore that's going to guide my synthesis.

>> Uh, that is a good question. I have not even looked at the linear stuff, um, even in the language. So, uh, um, but yeah, the way it works is it's using all of the information from GHC itself. And so, um, presumably GHC will tell me about the multiplicity of my arrows. And then, um, the trick is just to run the proof search sets that, such that it respects that. So I don't think there'd be any challenges there other than just writing the code.

>> Cool. And I mean, Wingman could probably write some of that code for you, right?

>> Like the more like the better it gets, the more I use it in daily dogfooding and, um, it's remarkable. How, how much, like, just how lovely it is, right. Compared to the bad old days where I had to write a case statement for myself and like, go look up all the constructors. Right. It's sort of stupid how, how much work that was. And I didn't realize because, um, just like the IDE situation was so bad for Haskell that. Um, like before Haskell language server, you just, it wasn't worth your time often to do it. Right. So it's, it's an amazing change in the last year. So the HLS guys are amazing and I wanted to thank you so much.

>> Yeah, well, like I mentioned, we haven't been able to get it working reliably with our code base, but uh, many of us have been working with it in our like side projects or whatever, and everyone that has it working just immediately falls in love with it. It's amazing.

>> Yeah, it really adds a lot to the language.

>> Yeah. We've been kind of waiting for this to come to the ecosystem because we've been kind of stranded as far as, you know, tools that we have in our tool belt. Um, and I think agile HLS really just, you know, hit a home, run more or less for the usability and feature fullness that we need in the Haskell community.

>> Yeah, absolutely. It's it's been like day and night. Just how quickly the tooling situation has changed the last year.

>> Yeah. And it's funny when we were talking to Matt Parsons a couple of weeks ago, he mentioned that since Haskell is such a powerful language, you can kind of get away without having a powerful IDE. Uh, but once you also have a powerful idea, you just kind of like leapfrog your own productivity. It's great.

>> It's crazy. Yeah.

>> Um, so could you tell us, uh, how did you come to work on wing man and program synthesis? What drew you to that?

>> Yeah, that's a, that's a great question. Um, I, so maybe two years ago I sort of fed up. I was living in Ottawa in Canada, which was an atrocious place and just sort of missing a lot of the intellectual community I was looking for. And so I decided I was just going to like run away and live on Haskeller's couches for as long as I could handle.

>> Yeah. I remember that.

>> So. Yeah. So I made it for about four months of like couch surfing and meeting all sorts of really amazing people. Um, and one of the people I met was James King, who had like a little tablet. Um, and he, he was sort of pitching me on this idea of programming on the tablet. Right. And I'm like, what? Like, what would you need to do to make that happen? Um, so w the dream I have is like one day being able to be out in the park, on my tablet, and like programming, like productively out in the park without a keyboard, without a monitor, without any of that crap. Right. Um, and so that, that question sort of got me thinking about like how, how could we find a better interface for programming that isn't just typing on a keyboard?

>> Right.

>> Um, at the same time, I, I was talking a lot with the Reed Mullanix who has been working on a tactic synthesizer for Haskell and sort of, he does a lot of. Things in like dependently type languages where, um, they have all the sort of this code synthesis stuff, and he wanted to bring that into Haskell. And so he had built like a bunch of really incredible libraries, um, that do most of the work. And so really my contribution was taking the, the idea and trying to bridge the gap there, right. Between the interface and the solution.

>> Okay.

>> Um, yeah, so that's sorta how I got started on it was just, um, This like, sort of being tired of being on a bus and trying to type yeah. Like having terrible RSI for the week after, you know?

>> Yeah. Um, it's funny, you mentioned different, uh, like using a tablet as sort of a different programming paradigm and I've thought a lot about that as well. I imagine a lot of programmers have of like, why is it that I have to be sitting here with a full-size keyboard in order to be productive? Um, and yeah. It seems like the interface for a tablet would be wildly different or like in VR or on a phone or really anywhere but sitting at a desk with a computer.

>> Right. I think the value of a keyboard is that it lets you type arbitrary strings. Right. But almost no strings are programs.

>> Yeah.

>> Right. It's sort of ridiculous that we even use strings to represent these things in the first place.

>> Right. And a lot of the strings that you end up typing, aren't arbitrary, they come from some other part of your code base.

>> That's true. Yeah. Um, even like, like keywords are, should be auto completable and like a lot of keywords you need in like together. So I need to, every time I have a case, I need the word of

>> exactly.

>> So why do I have to take that?

>> Yeah.

>> Right. At any given point, there's only like five things you might want to do. Right. So why don't we just give you those options?

>> I like it. Um, and I know a lot of people go down the route of structured editing as a, you know, solution to this problem of, instead of typing text into an editor, Let's have something like, I think scratch is kind of the prototypical example, but, you know, block-based where you pull that case statement out of some pallet and drop it in your program. What, how did you, or what kind of led you to program synthesis versus structured editing?

>> I think structured editing is a good approach. Um, I didn't know how to do that. Um, and I guess the other thing is like, even if you are, even if you have a better interface, like. Still, why do I have to code things that have exactly one solution, right,

>> right.

>> A huge purse. Like part of the reason I like Haskell is the type system is so good at constraining implementations. Right. And so I sort of look at like, you've done your job. Well, if, if there's exactly one solution to your type,

>> right.

>> That means you've designed a good program. And then let's just find that thing.

>> I like that. Yeah. That's good. Cause I'm trying to imagine, like in JavaScript, what would program synthesis look like? And. It seems like, yeah. I don't know. I don't know enough about it.

>> Yeah. I'm not without crazy AI.

>> Yeah. Or maybe with TypeScript, there might be enough ins there.

>> Yeah. I dunno.

>> Um, actually we use a plugin called, uh, tab nine. That does a much, Oh, are you familiar with it?

>> Uh, I, I sort of know it exists. It's sort of like machine learning.

>> Yeah. It's very, I don't know how to describe it. Maybe like stochastic, where it just looks at the strings in your code base and figures out how often they occur. And then when you start typing something, it's like, Oh, normally when this is before the cursor and you're typing this, this is what comes after. So it'll suggest that it

>> Dies it work well.

>> Pretty well. Yeah, especially for pretty rote stuff like imports or again, HLS solves imports where you, but if you are typing one out, it'll be like, this is a typical module name. Here you go.

>> Cool.

>> Yeah, it'd be nice to get the more time invested in figuring out how to make HLS work in our program, but for the time

>> Do you use a lot of template Haskell.

>> We have a little bit where you're using more storage, we've turned toward using more of the persistent, uh, quasi quoter for doing our models. So yeah, that's

>> often that that's the big issue. Um, and if you can sort of separate that into a different package, I suspect that will solve your problems. But I can't promise

>> we have somewhat, I mean, like everybody, we have a bespoke environment and we got Docker containers and we got all kinds of stuff going on.

>> Of course.

>> Um, but yeah, cam you use tab nine. I think more than I do. Ah, so you may be able to speak to like what it does, what it's good at. Especially in comparison to HLS.

>> Yeah. I mean, if you're making a sweeping code change across the entire code base, it can pretty much figure out what you're trying to type as you, you know, just kind of start it. So it's been really helpful. Um, you know, imports is one that is obviously, it has a lot of examples to analyze and say, Hey, this is what we think you're doing, especially because we have pretty consistent naming schemes. So it makes it really easy. Um, And, uh, you know, when you're writing function definitions, it can get a little tricky sometimes because it wants you to, like, if you're doing your type signature, like the next line, it tries to say, Oh, you're doing your type signature . Again, and you're like, wait, no, I'm not actually implemented here. So that can get a little bit of a note and a little bit of annoyance there, but right. Overall it's pretty helpful. Uh, just in the day to day, you know, I think if we can get some HLS love, then. Yeah, that sh meet the need for, that could go away, um, to be really cool.

>> It's funny. Cause they're kind of, uh, similar solutions to, or sorry they're approaching the same problem with radically different solutions. One is like very smart. Give me as much information from the compiler and I'll use it. And the other is like, I don't need to know even what language you're typing. I'll just guess

>> it's, it's amazing to me that that works at all.

>> Yeah. Yeah. It is startling. Um, so yeah, try that out. And uh, I'd be curious to see what you think about it. Um, but on the topic of program synthesis, I am aware of a couple earlier attempts with Haskell to synthesize programs. Like I think Lambda bot can do some stuff. And there's a package called djinn that does something similar is wing man built on top of those are related to them in any way.

>> Not at all. No, I don't know how Lambda button does it, but I know djinn um, doesn't work particularly well.

>> I've never used it. I just know it exists. Djinn will do a lot

>> of like, um, Like sort of const stuff like it doesn't care if it's used arguments is just like, here's a solution. Um, one thing that we meant also does that Djinn doesn't is recursion. And so Djinn or, uh, Wingman can like implement foldr for you, for example. Um, and if it, if it does recursion that guarantees that, um, it's, recursing on something structurally smaller, so it will terminate

>> productive. Yeah.

>> Yeah, exactly. Um, so Djinn I think is it's, it's interesting that exists and sort of, it was inspiring to me just to see that someone had made progress there. But, um, if you've ever like tried to use it for real, it, it falls short quite soon.

>> Mm.

>> Well, I hadn't tried to use it. I don't think it builds with more recent GHC so that's what prevented me from trying it out. Yeah.

>> There's um, there's another thing I've heard of called magic Haskell, which is sort of the other way is it says here's some arguments and here's what the output should be. And it tries to synthesize a function that produces the outputs from the inputs.

>> Oh, that's cool. So more kind of spec based.

>> Yeah, exactly. Um, I haven't, I haven't looked at it with the website was down when I tried to run it, but

>> that sounds really cool. Yeah. I've heard of similar projects. Um, I th I think I I'm trying to remember the name. There was a project in like scheme or something like that. I think it was called barley man, or it's been many years since I heard. Anyway, there was some presentation where it's like, you, you give a test case and it'll produce a function that meets that. And then you add another test case and it'll churn for a bit and say, okay, well I have a new function now. And as you add more and more test cases, uh, the implementation gets more and more, you know, don't look behind the curtain type implementation, but well, it works technically,

>> at least it gives you the outputs for the inputs. Right,

>> right. Yeah. And then, um, I think for those, that type of program synthesis, uh, Property-based tests will give you much more assurance that your implementation isn't something more than just a pile of this statements. Like if you give me this, I'll give you that. Uh, which I think ties in with algebra diff driven design to kind of take a corner here. Um,

>> that was a good segue.

>> Thank you. So yeah, property-based tests are, you know, a way to. State properties that should hold in your system and then test it against the implementation and see if it works. And algebra driven design is all about coming up with those properties, right?

>> Yeah. It's um, the, the book itself sort of the main thesis of it is that. If we're doing functional program, we should really be thinking about equality of programs. Right. That's sort of what it buys us over imperative stuff. And, um, and so if you're like designing some API, it's really interesting to ask when are two expressions in this like DSL or this API is the same. Right,

>> right.

>> And we're sort of used to this in everyday Haskel. We say like fmap dot fmap is the same as one fmap. Right. Um, but very often, like very rarely do you see people think about this for like the libraries they're writing and lesser, the category theory, people and stuff. Um, and so the, the claim is that, um, we can think about equality for like very mundane sorts of tasks. Right. Like very mundane, like real world applications that you're writing. Um, they, they should have equalities as well. And, um, so, so there's a few things that come from that, right? One of which is if you have these equalities, then of course you can turn them into property tests, and then it gives you like wicked amounts of, of just test coverage, right? For every property test, you can generate arbitrary many unit tests. Um, And so that's, that's exciting, but the other thing is what it does, is it constrains your implementation, right? Um, there's going to be sort of infinite, many ways of implementing a program, such that like all of these equality's hold, but often if you like chase the equalities, you can find different ways of representing programs. And so you can, you can use the equalities as a tool for as an implementer to say, like, I know that these two things are equivalent, but one of them is maybe faster.

>> Right.

>> So I'm going to choose that as my sort of basis. Um, and then use the, the qualities to rewrite all the things that user writes in a language that's, um, like useful to them, or make sense to them in a way that is equivalent, but faster.

>> Right. Okay. That sounds to me, that sounds to me like something that is very appealing to programmers, especially. I feel like this comes up a lot in like lisp programming, where people want a very small, like kernel of, uh, primitives and then build everything out of that. And it sounds like algebra driven design is trying to find, uh, maybe in kind of a roundabout way, find those primitives, uh, such that they meet all these properties and then you can shuffle them around behind the scenes to get a good implementation.

>> Yeah, I think so. I think that's a very good way of phrasing it. Um, one thing I'd like to stress is just that the implementation doesn't need to be at all based on the kernels. Right,

>> right.

>> The kernels are for the user, but for the implementation, you can have all sorts of crazy, like, um, specialized primitives that make no sense and user lands, but that's okay because they're fast. As long as you can prove the equality. It's fine.

>> And I think this ties in with something else you said from the book about abstraction, where. Programmers often think about abstraction as like hiding implementation details. And it does do that, but, uh, it seems to be more powerful when your abstraction is based on this algebra so that, you know, your abstraction can't leak because the entire, like the rules of the thing are based on the algebra you built. So the implementation kind of by definition does not matter.

>> And I think that's it. Absolutely. I think too many people think about abstractions. Like put it in a module, I'll put it behind it. Right. Or like I'll re I'll pull out this implementation to its own function. It's like, that's not, um, there's a quote from Dijkstra I really like, which is that, uh, abstraction is not about being vague, but about creating a new semantic level at which you can be absolutely precise.

>> Right? Hmm. Yeah. Uh, so yeah, yeah. I, uh, like I mentioned earlier, have not made it entirely through this book yet, but I'm really enjoying it so far. And it feels like it'll give me some tools for approaching problems, uh, particularly, um, taking the time before diving into implementation to think about the problem and kind of push on the boundaries of it and see where it can be broken down into simpler pieces, which is something that I've already seen, um, in the examples that you give, where. You talk about like, you can come up with a property and it may be very complicated in that suggests that you may have multiple things kind of mixed together there or complected to borrow the, you know, the rich Hickey speak there.

>> Right.

>> Um, and you would do well to pull those apart and then in doing so you might discover more properties about your program, or you might discover a simple, simpler way to implement it, or, you know, any number of things. So looking forward to continuing to explore that.

>> Yeah, well, uh, I think it's a great book and I'd strongly recommend, it

>> might just be a little bit biased, but I agree with you. Um, but yeah, that's not the only book you've written, right? You previously wrote another book called thinking with types. What is that one about?

>> That one is about all of the, um, all the wonky stuff you need to do in order to do type level program. I mean, Haskell, right. Um, w it's sort of unfortunate, that's such a book as necessary, right? Because if you look at languages like Agda or, um, Coq like properly dependently type languages, there is no T type level programming. It's just programming,

>> right.

>> In Haskell it's, it's sort of ridiculous that we have this like constraint kind where. It's sort of a tool, but it's not really, but it's like a set of constraints, but it's not data dot set. Right. And it's like, why does this exist? Right. So, um, so thinking what types of sort of a collection of all the folklore that has existed about how to do dependently type stuff or like type level programming, more so than more generally, um, without sort of needing to go through and find all the resources for yourself,

>> right. Yeah, I, uh, I often, w we have turned recently into using more, uh, servant the HTTP API library, which is very much implemented at the type level. And it definitely, uh, highlights some of the, I don't know, sharp edges on dealing with this type level of programming and Haskell, because you have to leave the very comfortable value level programming world. And deal with this entirely different world, which is kind of disorienting.

>> It's the same, but it's different.

>> Right.

>> And annoyingly.

>> Yeah. And there's all new terminology to worry about, you know, you got type families and data, you know, like just, I want to deal with functions and you know, the stuff that I know,

>> right. Yeah. It's definitely a mind bender to some degree. Um, you know, as someone who's not as experienced in Haskell, like w. Walking into type families and type level programming. Definitely. I mean, it's been insightful and fun to learn, but it definitely took, took a minute. So, um, yeah. Appreciate you taking the time to gather some helpful resources for that. Um, that way people aren't bouncing around. What do I do? What a type families, how does this work?

>> Yeah,

>> as an experience Haskell, or it doesn't make my brain bend. I need less. It's it's just weird. And like every single time I need to repage all these arcane rules for how to do it. And, um, as I get older and wiser, I sort of, the more, I feel like maybe this is a bad approach and like, maybe we just shouldn't be doing these things except in like very, very small.

>> Yeah. So do you feel like we should be. Pushing toward dependently typed languages, or we should be pushing toward more, like give up on the type level programming and focus on the value level stuff.

>> Um, I think either of those would be okay,

>> but we're kind of in the middle right now. And that's the problem.

>> Um, I don't know what the dependent Haskell story is going to look like, but I'm hoping. It will just work in the way that like lean or Idris just works. Right. Um, I hope it is. I, I want to believe, but based on what the current types story is, I don't know if I feel it yet. I haven't internalized it.

>> Yeah. I haven't, uh, Been following the dependent Haskell thread. I haven't played with really any dependent, uh, dependently typed languages. I'm aware of Idris. And every time I see a tweet pop up with it, I'm like, man, that looks pretty cool. I should check it out sometime. Um, But, uh, yeah, I'm not hopeful that Haskell as a language and community will be able to shift from not being dependently typed to being dependently typed. It seems like too much of a change, but, you know, maybe it will happen. And I think with, uh, linear types, that's a, that's a similar type of change. And maybe if that one goes really well, that could bode well for also doing dependent types.

>> Yeah. Is your concern sort of that there's like too much baggage or too much like. Ego or, um, or just like maybe the implementation won't be what we want, or

>> I would be afraid of baggage. Like we have so many things as bad as the type level programming situation is now. Um, people are at least familiar with it, you know, it's close at hand, uh, to continue borrowing rich Hickey isms. Um, and if we say, okay, well, all that is gone now and it's replaced with this thing that is better. But you have to relearn everything. Maybe that'll be too much and people will give up or maybe it'll be great and everyone will jump ship to, but I don't know,

>> the, the, the like dream of dependent types is that they work just like values. And so there is nothing to learn. Right.

>> Right. If you're already familiar with like the singletons library or like servant would have to be, I assume, completely rewritten and you know, maybe the

>> Servant's and amazing piece of engineering, but I wish it didn't exist.

>> Yeah, I think I agree with you. I really enjoy using it and everything that it gets us, but. Uh,

>> it's beautiful when it works well. And when it doesn't you get these like type tornadoes, like five pages and they just scroll all the way across several times. Yeah.

>> People like to give JavaScript a hard time for like the nested callback thing. But yeah, those servant type errors are, are much.

>> It's amazing when it works. It's so fantastic. Um, and if you can follow the happy path, it's great. Unfortunately, I find I'm not good at following the happy path often.

>> Yeah. We try to stay on it. Uh, I heard someone, I wish I could remember who, but I heard them say that like the. The best thing to do as a programmer is just, don't do weird stuff. And the hard part is figuring out what the weird stuff is. So yeah, with servants, as long as you stay on the straight and narrow, then it works great. But otherwise, yeah. Um, but yeah, I don't think we're going to get to the answer today of is dependently type task we're going to work or not, but I I'm just, um, I feel like if there's enough work involved with the switchover, then it's going to be a hard sell versus. Oh, well, I'll switch to Idris or I'll switch to, you know, whatever other language.

>> Yeah. Haskell has the advantage in that we have users, all these other languages are really cool, but nobody, nobody really outside of the core group of researchers and like some academics as far as I can tell, really use these things.

>> Right.

>> Um, and so I think it would be hard to, I think Haskell has momentum. I think it's probably past the, the, I think it will exist forever.

>> Right. Um, in one way

>> in one way or another. Right. Um, so I, I think that's promising and, um, I'm really curious to see how they deprecate the old stuff for when dependent type Haskell happens. Right?

>> Yeah.

>> Do you still support all the weird type family stuff? I guess you have to, but I think it's weird semantic that's right.

>> Yeah. I mean, given how GHC in particular support stuff now, um, It seems like they would support it for quite a while. You know,

>> that's a very good point that that actually scares me more than

>> GHC seems to be very, um, and, and probably for the best, but they seem to be very hesitant to deprecate anything and get rid of anything.

>> I mean, it's, it's, it's amazing if you're a user of GHC, it's less. So if you are like a revolutionary. And I want to change the language so I understand why they do it, but I wish they wouldn't, but I don't, you know, if it weren't there, I would miss it, I guess, is what I'm trying to say.

>> Right. Yeah. Um, so yeah. Uh, thanks for explaining, thinking with types to us, it sounds like both Cam and I could do well to read it and maybe, uh, understand what we're doing with servant a little better. Um,

>> I think it would probably help if, uh, if you're just sort of bashing your head against the wall, why doesn't, why doesn't this work. Whereas, and,

>> um, but yeah, I'd like to, uh, shift gears a little bit and talk about your polysemy library, um, which maybe is a little old hat by now, but, um, yeah. Tell us about it. What is it why people may want to use it?

>> Yeah. Um, so polysemy is free. Monads, um, done better, I guess is how I would phrase it.

>> Okay.

>> Um, and so the idea is sort of, you can abstract away from a specific monad stack, uh, like a monad transformer thing. And instead you can say, ah, I have these effects in scope and these effects can be like really fine tuning. Cause they like, I have a connection to an FTP client. Perfect a FTP server, or I have like, um, I have the ability to read and write to some data source. That is a key value source state fully, but I don't care what that is. Maybe that's uh, uh, yeah, so. Um, so the idea is sort of, you can separate your business logic, which is I have some abstractions I care about from the actual implementations of those things. Um, that's the sell at the high level, and I guess of all of all effects systems and, uh, and then later you can choose how to interpret those systems. And so I can say, Oh, I have this, this key value store. And like maybe that's Redis or maybe that is HTTP requests. Or maybe it's a local file, right. Or maybe it's just a local state monad, um, it, the, the application shouldn't care.

>> Right. You only care about the interface that it exposes.

>> Yeah, exactly. Like, and so, so the pitch is sort of like, what did the business people care about? Can we express them in 10 lines of code? Right. And generally if you're at a high enough, high enough level of abstraction, the answer is yes. Um, and, and that's really lovely. Right. But when you get to a point where all of your business logic. Is comprehensible. And then you sort of transform it through these transformations of, I have this one effect I can implement it either directly, or I can say I can implement it in terms of other effects. And so I can say, I can implement this state, but only if I've got access to a web client. Right. Um, but then that web client, you might also want to mock. And so it's not actually talking to the web, right.

>> Right.

>> Uh, so, so that's sort of the, the idea, um, polysemy, what it brings to the table is makes it much easier to do these sorts of things, um,

>> easier than what

>> easier than, uh, there's another library called like freer-simple and freer-effects and freer. And, uh, there's like 20 different free monad libraries in various States of, uh, love really. Um, and the idea for this was I wanted it to be, um, easy and fast and give good error messages. If you screwed something up. And so that those were the goals. And, um, the last one in particular was quite challenging. Uh, it requires like it requires a plugin to run, which in retrospect was a bad idea. Um, cause it means that you just have to keep that up to date with GHC versions in a way that like a library doesn't need to be

>> right. Wait. So it, it requires a plugin in order to work at all or in order to get down there?

>> No, not in order to work at all, but in order to, um, to like get type inference working. Hmm. Okay. There's a lot of programs you'll write in polysemy that without the plugin, you'll say, obviously this is what I want. And it's like, Whoa, I don't know what this effect is. And be like, there's only one effects. There is clearly that one, but it doesn't know. And so there's a, there's a plugin that like solves those. So it's sort of a type checker addition.

>> Cool.

>> Yeah.

>> Um, but yeah, I, uh, I can appreciate that. Keeping up with the GFC API is a little tedious. Um, we were just talking about how good they are at maintaining backwards compatibility. That's for their, you know, the compiler and everything. Not for the internals, which shift around much more often.

>> Right. Um, on the, on the other hand, like I appreciate it. I wish there were a better compatibility story though. There's like the GHC lib now, uh, which I think solves this problem. I've never really worked against. I think it's newer than. My issues, but

>> yeah, there's the GHC library for like parsing, right. That, uh, Shayne Fletcher, I think maintains. Um, and yeah, that seems really nice to say like, okay, I don't really use all the particulars or I can do a, uh, pretty straightforward mapping between all the versions. And he has done that for you.

>> That one, unfortunately doesn't work if you also need GHC the library.

>> Right.

>> Um, because, uh, the parser has just redefined all the types of needs. Which is lovely, except when you now want to talk back to GHC it's like, Oh, my expression is not the same as your expression, even though it's identical. Oh, great.

>> That's unfortunate. Yeah.

>> Yeah. So, um, okay. I think it's, it's a much better state of affairs than the old like source extensions situation was. Um, but I haven't had the joy of working with it yet.

>> Yeah. Um, Uh, I will say that it's nice to have the option of writing these plugins, you know, and I think that, uh, there are a couple kind of big name ones, I guess I can only really think of one, the record dot pre-processor has kind of like a preview of language extensions to come. Um, but interesting to see them used here for an effect library as well.

>> Yeah. Um, I think these days, I don't really endorse free monads.

>> Okay.

>> Alexis, Alexis King wrote an article maybe this year or maybe last year. It's hard to keep track

>> time as a flat circle. Yeah, it's weird.

>> Yes. I'm talking about how all of my claims for performance were untrue and, um, She was absolutely right about that. And unintentionally, unintentionally untrue. Right. And I wasn't going out of my way to lie about it, but, um, some issues sort of in the benchmarking and how the simplifier works and just like, there were several systematic errors that led to my performance claims being untrue. Um, so that was part of it. And then, um, The good news, I guess, or bad news, depending on how you look at it, as it sort of all effect systems have terrible performance, including MTL, and nobody noticed because everybody's bad at benchmarking.

>> It's a hard thing to do.

>> Yeah.

>> Yeah. It's not to say like, MTL is as bad as puts to me, but, um, so on one hand, like I claimed the performance doesn't really matter for most of the things we write. Right. Most of the time you're waiting on a network call or, or, you know, IO or something. So usually it doesn't matter, but it's, it would still be nice to get that. Right. Um, and on the other hand, um, the thing is I realized, I think we're all better off just sort of mock, like writing pure programs. If you just push all the effects as far out as possible, that's just a better solution in general.

>> Yeah. Um, are you familiar with,

>> Matt parsons actually has a lot of like good articles on how to do this

>> right now? The three layer Haskell cake, I think is one,

>> um, that one I'm not as Fonda, he's got one called invert. Your mocks.

>> There you go.

>> And that one is sort of all about how to like pull out the pure parts of effective programs and I really endorse that

>> yeah. And I think, uh, there's some, I I'm drawn to that, uh, approach of designing software because it extends outside of Haskell as well. Uh, if you're familiar with Gary Bernhardt, he has a talk about, um, uh, what is it? Imperative shell, pure core. That may not be the exact wording, but like yeah. Push everything to the outside. And then on the inside, you've already done all the network, all the database, all that. And you just deal with the pure stuff.

>> Unfortunately, humans seem bad at writing code like that, especially when like time pressure arises and it's like, Oh, I just need IO here. I can't be fucked to do it the right way. Right. Um, and then over time that stuff accumulates and sort of, I think that was really what I was rallying against with polysemy was, um, I had worked in like a pretty atrocious code base professionally, which just the entire thing was in IO and there was no. Sort of, um, discipline anywhere about what things were pure and so just like we, we found a multi-million dollar bug that bit us, because we just couldn't test anything. Cause it was all in IO.

>> Yikes. That's pretty bad. So I can see why that would motivate you.

>> Yeah. The problem is sort of motivation. Like these are, it's only ever after the fact, right?

>> Yeah.

>> Nobody really cares. If you say, Hey, everything's an IO and it's going to cause us millions of dollars, but it doesn't work until it happens. Right. So

>> right. And then when it happens, you get the, uh, the peanut gallery on Reddit saying like, ah, you could could've, you could caught this.

>> Exactly. Yeah. Um, so yeah, so I think it was, um, it was a really interesting project for me to just go through and learn how to do all of this stuff and really flex my type level. muscles.

>> Yeah. You can say lots of type of programming in there.

>> Yeah, exactly. Um, and I'm happy that it's taken off, um, in a way that I didn't expect. Um, I think that's exciting to me and also a little scary.

>> It's scary how people are using yourself.

>> No, because how I would like to write programs anymore. I think I've, I've learned something now that I hadn't learned back then. And so. People using that sort of reflects like either I'm wrong now or right.

>> And neither of which is a good place to be.

>> Yeah, exactly. And so I'm not sure what the answer is, but, um, anyway, so I'm happy people use it. I'm happy I get the credit for it. Uh, and you know, there's worse things in the world than people using your software.

>> Yeah. Uh, I'm I'm curious, we were talking earlier about, uh, dependently typed programs and how. You know, Haskell is kind of halfway there and it's awkward. Um, I have a passing familiarity with pure script, which has sort of an effect system baked in thanks to the row types. Uh, um, do you have any experience with that and how does it kind of stack up against the free monads?

>> I don't have really any experience with that. I didn't know it existed. And then they sort of chopped out of IO. Yeah. Kept the row types. And I don't, I don't know anything more than that.

>> Yeah. Um, again, I only have a passing familiarity, so apologies to anyone in the pure script community if I get this way wrong. But, uh, from what I recall, they had, um, or they have row types, uh, so they can do like anonymous records and those also exist at the type level. So you can have. And anonymous, uh, map of named things too. Uh, I think they just called them effects. So you'd have like some kind that represented. I can talk to the database and your function and say, okay, I need this effect in order to work. And I think they don't do that anymore. You can, if you want to, but like officially they effectively just have IO as their effect. Um, so it was, uh, interesting for me to see like, okay, they have all this power, they can express all this stuff at the type level and. They kind of don't want to, um, and they'll go back to doing things the way that Haskell does it.

>> Yeah. I don't know why. I didn't maybe, maybe they've tried it and given it a go and realized, Oh, it doesn't work. Um, maybe just like Haskell has the prestige and there's this weird monad thing where once you realize, once you learn about monads, you need to write about them.

>> Yeah.

>> And like, I, I think that is a big problem. I don't know if that's relevant here, but I think I could see that happening where like someone says, Oh, monad transformers let's use those because Haskell uses those. Um, again, I don't know anything about pure scripts. I don't know if that's the sentiment they have, but, um,

>> so, uh, to try to shove these pieces together, I think one of the problems that PureScript ran into was that, um, if your effect kind like the thing that says, Hey, I need to be able to talk to, or write to the console or read from it or whatever, if that isn't shared among every library that you're working with, then you get this very strange fracturing where you have, let's say two different Redis libraries and they each define their own effect. And so if you have one and you want to use the other, suddenly you have to like redo all of the effects all the way up your chain, because you have both of them now. Um, and I, I feel like Haskell also can have this problem where like,

>> absolutely we do,

>> you know, if some fundamental type isn't defined low enough, then everybody defines their own and it becomes a zoo. Um, and maybe that's just way more annoying to deal with when you're at the effect level.

>> I think that's true. Um, I'm hoping that people don't, I guess that's one of the things I liked about polysemy it was sort of the high level idea of like, I just have some key value state. Right. Um, the thing about if you have like a Redis effect, is that the only implementation of that can be Redis

>> right.

>> There's you can't do anything other than like Redis or reimplementing Redis

>> I mean, you could try.

>> Yeah, I could try, but at that point, why right,

>> right.

>> Um, and so. I think there's a value in like, keeping your effects as small as possible exact exactly. For this reason, regardless of the system, or like, if it's just MTL or even if it's just like making a monad stack a concrete monad stack of just like keeping your effects as small as possible, because otherwise you're making choices that you're going to have to live with. Right. Um, and unfortunately, like you have to make choices at some point, but again, if you can push them as far out as possible,

>> Yeah,

>> that makes life easier.

>> I agree with you, but I'm not surprised to hear you say that based on algebra driven design. Cause it's like, you know, if your interface is I am Redis, then it's really hard to come up with properties about that to mock it, to do anything. But if you're interface is,, I'm a key value store. Much easier.

>> Exactly. Yeah. What are the properties of Redis? I don't know if there are any right. Guaranteed to get back what you put in.

>> Yeah. Uh, yeah. Um, well, we've covered a lot of good topics here. Uh, Sandy, is there anything else, uh, you know, what are you working on? What are you looking forward to? Uh, what's next for you?

>> Yeah, so right now I'm working like full-time on a Haskell wingman. Wingman for Haskell that branding is still being figured out,

>> up in the air.

>> Yeah. Yeah, exactly. Um, and so I'm trying to make that, like my full-time life. Um, and so I've got a Patrion for that if, uh, if anyone's interested in helping support me through that,

>> for sure. Um, yeah, that's sort of linked to that in the show notes.

>> Marvelous. Thank you. Um, that's like where all my time's going. I'm putting like 10 hours a day into it right now.

>> Wow.

>> And so, uh, yeah, besides that, um, I think that's it really like, that's all I'm doing. It feels good. Honestly. It's nice to have like a project you really care about.

>> Yeah. And if people want to find you online, where should they go look for you?

>> Yeah, I'm, uh, I'm online at reasonablypolymorphic.com is my math blog. And I also have sandymaguire.me, which is my personal blog. And it turns out like, I'm, I'm going to shill them both, but there's really no market for like, there's no intersection of people who care about both of those things. People care about my math stuff, or they care about like me as a person, but I learned that the hard way. And you just split them up, but I'll shill them both. And, uh, I think that's, that's pretty much all my online presence.

>> All right. Well, yeah. Thank you so much for being on the show with us today. It's been great to have you here.

>> Oh my pleasure. Thanks for having me. And I just want to thank you both for like all the great things you've been doing for the community.

>> Thanks. I appreciate it.

>> Gonna we keep on keeping on.

>> Yeah.

>> I like that. Cheers, please do.

>> Uh, and, uh, thank you to the listeners of the Haskell weekly podcast. Um, thanks for tuning in, even though we're not here every week, we're here most weeks. Uh, Uh, I've been your host Taylor Fausak and our special guest this week was Sandy Maguire. Also with me today was Cameron Gera. If you want to find out more about Haskell weekly, you can visit our website, which is HaskellWeekly.News. If you like the show, please rate and review us on Apple podcasts. Uh, and if you have any feedback, you can tweet it at us. Our handle is @HaskellWeekly. Um, and yeah, we're elsewhere on the web, but those are the main ones.

>> Yep. And Haskell weekly. Yeah. Brought to you by ITProTV, an ACI learning company and our employer. They would like to offer you 30% off your subscription by using promo code HaskellWeekly30 at checkout. Um, so if you're ever interested in it, cybersecurity training, Yeah, we have anything and everything you need. So check it out if you're interested, but I think that about does it for us Taylor and Sandy.

>> Yeah, sure. It does. So thanks for joining us and we'll see you next week.