ETHWarsaw 2023: Miao Zhicheng, Superfluid Finance - Pure Functional Solidity for Fun and Profit

M uh will present uh on solidity so let's welcome me wormly in woro I thinking it should have be Lou uh okay thanks everyone for coming this talk and uh it seems there are some people interesting about functional programming right so uh so quickly uh my name is me I co fed a super fluid and you may find me with my funny handle that I inherited from my childhood hellwolf from various place except Twitter um okay so I'm going to talk about functional programming in solidity today and uh so uh the goal of this talk is uh demonstrate the possibility of uh kind of limited functional programming uh in solidity and showcase um a example of using this Paradigm to build super token I don't know if I show that today but make you interested also in functional programming so first question of course is uh uh who here thinks uh like know what is functional programming in general and the okay and also practice it to some extent okay good I have a good crowd here um so a quick example uh in solidity right so how how how it looks like so well it looks like normal solidity but with a few uh that I kind of separate in three sections first uh section uh is uh um kind of pure functions um so you call those underscore pure functions it return a data structure and uh that's kind of retrieving the data no sorry those are not few functions those are like a retrieving the data the second section like shift flow that be like the pure function which you send the structure inside and do some transformation return A and B I'll show that in a moment there's something tricky about memory um then in the last section you just uh uh apply the uh storage uh operations right so kind of kind of it's still solidity but it's uh you separate the pure logic per se right so that's just quick example let me let's dive into what the what are actually uh what is about right so what is functional programming let's start with that uh so the way I see it is that the functional programming is really about uh more uh describe your program in terms of what it is as opposed to say how you should do it right more declarative as opposed to uh pres prescriptive or imperative like describing how it step by step how it's down right so more what and let how right um so Implement as much code as possible in kind of in data definitions equations and the logic formulas or sometimes called properties um and for the for this code kind of strictly pure functions are your friends uh because kind of referential transparency that's a word uh people use in the fun FB Community functional program community so kind of same input same output you are guaranteed with that I use a word uh explicitly say strictly pure functions but in solidity you you you you you might know you should know that uh there's pure functions but it's deceptive it's not strictly pure because of memory stuff I'll show in a minute what do I mean so it is really about deferring the side effects so what are the common side effects the storage access is definitely uh side effects whenever you access storage you lose the ability to have a referential transparency right so that means that uh uh you can't guarantee that when you call a function you get the same result because you're accessing something that uh is outside of your control often and uh uh other things like Integrations with the external code Like Glue code like for example you call Unis Swap and do something right those are kind of external transactions and those are the uh interactions that kind of uh I computation strategies is more abstract sense right so uh when you describe bunch of equations there's nothing said about how those computation are are performed in which sequence is it in parallel is it in sequence right so computation strategies is also part of the side effects which is uh a bit more abstract and probably less obvious often um so to make the code Act use for implementing the computational strategies right it's needed so what are the computational strategies um most of language has it builtin you don't even notice right like solidity any other imperative language JavaScript or something uh you you take it for granted when you write a code you know that okay this code is going to be executed before that that right so kind of taking for granted um typically sequential also right uh some people may call it Mo will explain what what does mean in a moment uh but the thing is uh things can be concurrent and kind of like graph Computing right so think of I think the best example I would give is like your spreadsheets when you write things in spreadsheets write formula or anything you don't write okay which cell should be calculated first it's all just dependent graphs right so when you change one cell any all other formulas dependent on that cell will also get updated so in that sense it is concurrent right so there's nothing said about how the cell should be calculated you don't write that as a spreadsheet maker right so uh that's where in a computation strategy also it's kind of abstracted away but uh with normal programming language you don't get that uh apart from kind of more pure functional programming language so uh now abstracts stuff going away we talk about why functional programming right so uh I think the best paper the classic one would be from John Hughes um really recommend anyone haven't read it read it because uh title is why functional programming matters right title says itself um so it is a gateway drug to the functional programming so going to repeat myself um so one of the quote I'd like to give is uh from the paper is that as a software becomes more and more complex uh it is more and more important to structure it well and well structured software is easy to write easy to debug and provides a collection of modules that can be reused and to reduce uh future programming costs right it's very passionate about uh what I said there and I think for the smart contract space is especially important uh this principle I mean uh in the bull market we want to move fast and you know break things but uh when you actually want to take over the world with this new Financial system right you might want to take it more seriously than than that so uh it is important to kind of learn from the um some of the past like great minds about this I think this this is really a uh how to manage complexity and how to make sure that your uh smart contracts uh is under control control is more you know secur ultimately right the keyword is a better debugging better reusability and less maintenance costs right so um and I I claim I would claim that uh I claim that it is uh the best way to structure smart contracts but it takes time to get there because we um well there are a couple of language of course but I mean most people still using solidity right so let's see how far we can get with solidity to try this programming style so that's what I want to achieve here today uh uh should I say something about this um uh I mean how do we nowadays test our stuff right I mean some people say testing production right okay good for them uh but uh but maybe uh in smart contract if you want to deal with people's money we do a lot of extensive testing right so before you go out before you kind of deal with other people's money you might want to test a bit more right so uh M has some limited post production formication I don't use a correct word here unfortunately I need to change that uh so people you may know about uh tools like sea right they provide this uh C verification language they can help you to provide more Assurance after the testing right because testing don't necessarily address everything uh because it's manual right right but you have a from trail of bits they have uh tools such as Aida if you heard of it's a kind of great fuzzing Tool uh that can automatically help you to discover uh more cases without you to write a lot of code um if nowadays in Foundry you also have an invariance test which does kind of similar thing but I think akina goes way way ahead I would recommend you to have a look from the trail of bits called Akida a e c h i DNA a if I spell it correctly yes so but the other approach would be more kind of correctness by construction what does it mean that when you create a code you try to have have as much as correctness built in right so I think I think functional programming is one way to uh getting closer to that right so that's much more sophisticated way but uh if you structure the code uh in a more functional uh programming way you are getting closer to more correctness by construction but uh and let me give you more example as opposed to talking a bit too abstract uh so what about solidity uh well solidity is nowhere uh near being able to kind of Express all the functional programming ideas but uh we can emulate uh some of the ideas so here are some of the technique that uh I I have been using in some of the production code right first of all there's a uh custom type so you kind of have bit more type uh uh um type system facility from solidity since uh uh I don't know when the custom type is from from 8 point something right but there's another thing called operator overloading it's seem like 8.19 this is one of the little trick you could use right so as example uh so here you can define a type uh it's not alas actually type wrapper in this case for the int 128 you define bunch of uh uh functions they call it free functions which is a confusing word I call a free range function meaning that this function you can deci Define outside of the uh contract SP globally Define them uh right those are look fine you have a pure return which is pure function uh then the last one is 8.19 introdu it's called Uh operator overloading so you know to make it easier simpler to use I guess uh so you can have redefine the plus and minus uh operators for this particular data type right so this will help you to make the type little bit more uh type information more strong so that you don't uh you can't do more than know what you define here so that's one small technique it may be trivial to some people but uh but it's important I think to to make sure that you get as much out of your uh compiler as much as possible right so um and unfortunately they did only halfway right so if I need to mix different types let's say you I want want to multiply the flow rate and time right if you multiply rate and time you get what return of value but unfortunately so don't don't allow that uh uh U type operator overloading so I kind of just using this external Library trick right to uh you can export uh this function globally and tie to that uh particular type so now I can do like FL R do ml r. multiply time right so it's kind of so far it's only syntactical right but let's go a bit more than that I'm talking about now the strictly pure functions right so not just the pure function synthetically from the solidity but strictly what what do I mean here so I would Advocate using this programming style you clone everything I know some people are going to S what about gas C let's not go there so referential a reference types passed with the memory keywords can be kind of modified by the pure function which is weird uh but but that's like JavaScript right you pass the object even if it's you know const you can change it but that's kind of the idea from there probably when they did it but if you want to have a referential transparency you want to avoid that so what you do is create a a boiler plate function called clone so each time you get a memory object from somewhere you clone it and so you you make sure that you you never change the input right so you kind of force yourself the kind of coding style people argue about a gas cost but I'm going there uh in fact it's quite small if you measure it uh so unfortunately there's no General way of doing M Copy per se right so that means the boiler plate code is a bit uh slightly annoying but you only need to do one clone for each uh object so uh sorry structure type so uh it's kind of manageable but I I wish there is more General M Copy kind of uh function so that I don't have to do this spoiler plate small thing all right so uh an example right okay so this rtb function meaning real time balance function so you have input which is u a structure called basic particle then you have a time so basically are calculating of this very abstract data type per se at this time what value is it what balance value is it right so uh so you you access the uh flow rate and you multiply by the time Delta and you plus the set thir value right so that's uh that's kind of the oneliner uh equation and the set of function there's a a. clog as you can see there so that's the trick that you make sure that you don't touch the input memory right so make sure it's become strictly pure right so to force yourself to have this kind of code St in way right so it will it will benefit a lot uh if you keep doing that because then you kind of uh have a much stronger refer referential trans referential transparency uh when you write solidity but you have to follow this because solidity don't offer full kind of support and you have to force yourself to do something like that okay so now we have uh something like a still kind of you know uh not so alien-ish but uh let's see an example let's generate some tests with what we have uh so far right so this is uh using Foundry that uh I say okay I want to generate bunch of random like using The Foundry Plus paing right I have uh randomly generated M1 I think it's time X1 is probably the let me check uh operating one uh yeah I think that's the uh the value right so so there's so if you see the function signature there's bunch of value generated by by Foundry randomly and there's two uh function pointers uh for does Act ual for for doing the actual uh test generation so I have this more General equations to uh uh assert the last assert is the most important right that's what I want to assert I want to assert what whatever operation you do in the end the property holds which is everything sum up to zero right so that's what what I want to test but how do I generate all the test I just passed uh the the functions like U uor shift 2 Shift 2 then the second one would be uu FL FL two flow to flow to shift two shift to flow to so I use one generator function to create uh uh four new different cases it's kind of like the the high order function insulated you can do that but it's it's ergonomically it's not that great but uh uh but does help know less boiler plate when you write uh generator um uh test cases for example uh right so what's a Playbook uh The Playbook would be that uh uh you define the data structure uh perhaps uh with the help of custom types also uh you define the colone function right so if there's M Copy that would be great um but they don't so create a strict pure function for the data uh like like basically your data transformation function but these are all strictly pure functions um U now the the very important part is finding the kind of properties and write test for these functions because now you have strictly pure functions then you can write the property you want to test and now Foundry has great support for uh uh almost like um property based testing right so uh yeah using that and test all the equations you want sorry yeah yeah thanks thanks for the question uh I didn't want to explain that because the time limit but in this case uh it represents uh uh the balance of account which is dependent on the Block time let's say the block time is the uh the time settled at so that when the time moves your balance also changes so this is a data structure to allow that to happen and this data also allows to implement Implement additional uh operations such as Shifting the value which is transfer basically and or flow meaning that you're connecting two accounts you flow the balance from one account to the other yes yes you need to save the necessary data in order to uh allow you to implement these uh uh operations uh so far we don't touch any storage yet so far it's all pure memory data right so so we we're good right we're not there yet right so uh I think I'm have only few 10 minutes so I need to be a little faster sorry okay so first example the property would be uh ADM potent right so I if I settle the uh there's a settle function right if I settle the the the data twice it should retain the same thing that's what it means at item poent I guess uh so you setle twice with the same value you get the same thing so you never get a different value uh then you have a associativity law right if you uh if you uh do the operations with a bracket like uh bracket in the first two versus the second part then you should uh you know equal to each other that's another property is important for the data for the data I might not have time to go there but if you are familiar with some of other functional programming stuff you might uh have some uh memory of that uh so now we come to the important part now we have uh bunch of equations uh but they don't touch any data so like what are we doing right so we can't really go to the uh blockchain right so uh now I have to mention the most dreaded word in functional programming the m word it's so called Monet uh and basically in simpler words is uh uh how how can we make those pure functions actually work in blockchain so we kind of have to sequence everything in a in a in a sequential way right so we run one function after each other and apply some storage update so one of the way to uh Achi uh kind of emulate that uh Concept in solidity is to implement uh uh getter and Setters but as virtual pure virtual functions and do they call Pure vir uh just virtual functions in abstract contract right so you defer the uh the implementation of that to the to the final to to to the to the final contract so this way you can implement this abstract contract without having to specify how that's actually done so this become reusable so the idea is you want to make a sequential Computing uh strategy that is reusable for other people right so uh okay fairly abstract so far I hope this one can can show you right I think back to the the first quick example I showed in the beginning of the talk um so in this case I Implement a reusable do flow function this is no longer pure function this actually does the computational strategy right so you load some data which is virtual function so imple the one that using that contract has to implement what is a get flow rate what is get this Index right you load those data as memory you pass that the memory structure to the shift flow uh pure functions you get the new uh data out and then you apply the storage right so uh storage update so so retrieving data do some transformation and update that becomes kind of reusable building block uh by by by by thanks to the uh virtual function but this just one way of uh doing it there's other way uh which I actually skipped um so let me just do a recap I not go there uh so the Playbook is you define the data uh you define the stricted P functions for those data for transformations and you find the property and the right uh test for those properties uh then you stitching together with kind of a strictly separation of the pure functions and the side effects especially the storage one and uh and and that's it right so that's that's kind of Playbook that's as far as we can go with solidity uh as far as I can tell right so okay so can can I do this in production uh I claim we can because we actually do right so yes I'm from Super fluid again so like that's what we do for some of the code so uh the super token is basically kind of Y 20 but with additional uh capabilities um so we we have upcoming feature uh called uh GDA which I didn't explain General Distribution so it's like you can distribute from one account to any number of accounts in streams right so in one transaction or update the one transaction so uh so that feature is actually entirely implemented with this new new paradigm um we have also actually Cairo v0 implementation they call the VZ I think I think V1 is totally breaking everything that's as far as I remember uh so the V2 or whatever V3 implementation might we will definitely use a new strategy uh if you're using solidity so yes you can do that in uh production and I claim I I encourage actually to try that out and uh um uh one side story is that uh I actually used some of the SRA tool and I can say for sure that uh it helps with uh the formication using Sor for example uh you can find the code example even the Sor verification code from our repo um so a teaser right uh just for today the talk so can we use solidity U instead right so so far we talk talk about using solidity directly uh but maybe we can just use you but using a different higher level functional programming language to kind of transpire to you directly as opposed to using the solidity right so uh just as a teaser you know I'm actually working on a project on that can show that if you have if you're interested after the talk happy to disclose more um so I'm kind of one time so thank you for listening so let's make solidity code better using functional programming now okay thank you uh the transcript can be found from our monor repo and in the wiki area you can find the transcript uh yeah any questions happy to answer any yeah uh can you explain a bit more that uh eff parameter that was seen in the yes uh I think I maybe overdid it that one um do you have more specific question about EF what does it mean or yeah like what exactly it's used for uh looks very madish when it first appeared but not exactly yeah okay so all right yeah I I I good question because I did uh skip at the explanation because when you do a virtual function here right uh but implementation might attach some special context because otherwise I might lose I mean if I want to store to some specific uh storage or whatever that context has to be provided that's why it's kind of opaque bytes memory the eff name here so I'm I I kind of overdid it uh it should be just a context so uh because then the virtual function implementer can put whatever the context uh they have so they have information regarding what's related to this so that's kind of the the case but actually the eff name itself you know about uh if you know about algebraic effects that's kind of what I taken the name from right so there's a alternative implementation actually if you dig into all code base I actually did a token F which has bit more strange way of doing the the the the reusable code but I didn't show it here because that's bit too esoteric uh but that's kind of the idea from yeah yeah sorry let's get you mic I understand that you started doing functional programming in solidity because it is your extensive background and it was easier for you to write functional code than regular code so what amount of years did you do functional programing before starting doing that uh okay so as a confection I started uh right I started programming there's only there was only probably two programming language I considered serious c+1 and Pearl and uh so that was you know the days I I'm not a computer science background I mean I started computer science more more like a computer science and engineering so what we were told to learn is C++ Pearl Java all this kind of thing uh but uh as as I my career moves on then uh uh uh then we uh got to learn more and more functional program get into in touch with functional programming more right so uh in I used to work for T and uh they had a uh extensive use of Scala at some point so a lot of people advocating uh SC Scala went to work for Tru and that's kind of where you know lot people talk about Scala Scala is like a a a wannabe higho in the jvm word right so that's kind of the uh uh the the the the thing so but personally uh I always uh kind of aspire to do the functional programming but uh uh only in kind of recently start to kind of dig really really deep into it profession Hol uh at the moment the quite okay yes I would say yes yes I actually my secret project will is Italian Haso so if you're interested we can talk about that later yeah you might not like my question but anyway uh the gas cost yeah do like this approach uh the benefits of this approach outweigh the potential extra gas cost so uh I did measure and uh even by by simply knowing how the memory copy uh gas cost is I can tell you that it's insignificant in the grand scheme of things right so what I mean is for example the uh a reading a story is 500 and the WR new fresh stories is 20,000 right so that storage actually overrides the gas cost for most of the things external core also sometimes copy like passing the C data and the the me uh to the memory know and uh actually internally memory copy it's really low I mean I encourage you to find it out yourself I you know I don't take my words right I I claims really low but I might be biased but I i' say comparing to all other significant gas cost it is uh it is not necessarily a concern right but uh do verify yourself okay the final question yeah this is more like a comment so if you like uh functional programming uh you can do a husale smart contract in cardano and you can do list smart contract in many other blockchains so you don't need to uh stick to evm if you really want to torture yourself no I want to stick to evm word so I'm going to introduce uh something to evm someday yes maybe near future okay uh have you tried using compilers apart from uh the solidity W the more something like industry standard llvm with some uh custom uh back end for the evm or uh in general compilers uh out of uh uh etherum word solidity and so on uh what I have considered I don't know if it's matching what you are saying here is uh what I'm trying here which I said is secret project is I'm compiling a unnamed uh high level functional program language to solid it U directly then I can use because then I can use solid compiler to compile the solid U to the evm code right so I'm not creating anything new language uh you might be right but I think uh you may well be right actually so but uh I think uh there's engineering cost problem right so to creating more things is uh more expensive I mean by definition than creating less so uh I'm actually looking into creating a minimal but to achieve uh this right so I'm trying to find a middle way but I I think you you might be remot okay all right yeah thank yo give it up for super thank you very much