Adam: Hey, welcome to CoRecursive where we share the stories and the people behind the code. I’m Adam Gordon Bell. This is a FP interview, but I think it’s a really broadly applicable one. Today we’re going to talk about Swift, the iOS development programming language. But really, we’re going to talk about total programming. Total programming is a pretty cool concept. I don’t want to define it because we’ll get into that in the interview. Some languages make total programming easier and some make it harder but I think it’s possible wherever you’re programming and it really just leads to more reliable code.
In my mind, this idea of totality it’s kind of associated with functional programming but I don’t see why it has to be. I think of it as a technique you can use anywhere. And it’s just a super powerful guidepost. It’s kind of a great perspective for thinking about your program. Andre, who we’re going to talk to today, that’s what he wants to talk about. How this idea of totality and totality checking, it just led him to write better iOS apps. Andre Videla is a iOS developer and functional programming enthusiast. Andre, welcome to the show.
Andre: Thanks for having me.
Adam: So, you have a great post on medium about how Idris and type-driven development inspired you and changed the way that you write Swift code. So I’d like to start with some maybe background and then dive into that. So for starters, for those who aren’t familiar, what is Swift?
Andre: So swift is a programming language that has been introduced by Apple a couple years ago and is mostly used in the industry as a tool to develop iOS apps. People use it also to start writing server code to go along with the iOS apps. And it has some following on Linux also for general purpose, like command line tools. It’s a programming language that is quite interesting in a sense that is both very high level but also low level in the sense that you need to think about memory and you need to think about how you move references around.
Adam: How is Swift different from Objective-C, which was the previous language for iOS.
Andre: So, when Apple introduced Swift, they have this very great slide which says, “Swift is like Objective-C but without the C.” It’s quite funny, I don’t really agree with that, but it’s still very funny to see it that way. I think what they meant is that it’s all the nice features that we like to use in Objective-C or would like to use more of in Objective-C without the problems of having to deal with unmanaged memory and unsafe preferences, for example. So the differences are mostly, well are in the type system.
Objective-C has a very, I would say weak type system in the sense that it doesn’t really help the programmer a lot. It helps the machine mostly. It helps the machine knowing what to allocate, where, how much size it takes, just like C, the type system of C is mostly there for the machine not for the programmer. Swift’s type system is way better at helping the programmer, helping the programmer write down better specifications, better types, better abstractions, and therefore better code. So the difference are deep between C and Objective-C. The way they are close to each other is that they use the same run time and they’re used in the same platform that is iOS and they have the same “Parent” which is Apple. Other than that, they are very, very different.
Adam: Swift is garbage collected, is that right?
Andre: Kind of. People will be very annoying with the term garbage collection, because they will say that anything that is not manually managed is garbage collected, which in the trick sense is technically true. If you look up in your Wikipedia. Swift is what is called Automatically Reference Counted. The compiler will look at your code, it will look at all the declarations, all the definitions and all the constructors and put little counters that will say, “Oh, this has been referenced once, twice, three times, four times.” Et cetera. And put code, in between your code that says increment the reference count, decrement the reference count. And when the reference count hits zero, de-allocate this thing because no thing will use this reference anymore.
It’s a form of garbage collection in the strict sense that you don’t manage it manually but it does not have the drawback of what you see, for example, in more classically a garbage collected or programming languages like Java, where you have GC pauses, where the garbage collector, which is mark-and-sweep will stop your execution, look at all the references that you’re using, mark the one that you’re using and de-allocate the rest.
This incurs some latency for example in applications when you scroll down a table, it’s a classical example that iOS developer will tell you is, you cannot have smooth scrolling tables in Android because of the garbage collection. The GC will pause the execution of the program, look at all the references, de-allocate the one you don’t use, and then keep going, resume the execution. Swift doesn’t have pauses since everything is dealt by the compiler. Everything is dealt with a compile time and the execution never stops. It just keeps going just like a program rich in C or Objective-C.
Adam: That’s interesting. So in some ways, the compile time garbage collection, if you want to call it that, it’s a competitive advantage for Apple because their apps run more smoothly.
Andre: Yes, totally. It’s a typical iOS versus Android argument to say, “Oh, at least our apps don’t pause.” And it’s very useful when you make things like games because on the Android platform, whenever you start allocating, lots of stuff are very dependent on the resources of the device, which are inconsistent across all devices even iOS. You really want to have consistency in performance and the garbage collector of Java doesn’t allow this. ARC allows somewhat more predictable performance when comparing memory allocation.
I would like to note that, it’s not because you have mark-and-sweep garbage collection like java that you cannot have good performance, it’s just really hard to do. And as someone said somewhere [inaudible 00:07:32] I don’t remember where it was, but you can for example, in a mark-and-sweep garbage collected language, make a huge array of references and mutate them as you go and never allocate more resources or de-allocate resources because you always have a pointer to them. And that is very close to just having a huge buffer in C and boarding stuff in it. And someone said, “Whatever your programming language, if you want performance, it will, no matter what look like C because [inaudible 00:08:05] a buffer of references. You put stuff in there, take the stuff out, and that’s just what you do in C.”
Adam: Well, that’s a sad thought to me. You know what you’re making me think of is Rust. So how does the garbage collection in Swift vary from Rust?
Andre: Unfortunately, I’m quite unfamiliar with Rust. I’ve tried to use it once and I made a toy ray tracer. It turns out a making a ray tracer is not the best way to learn Rust because I don’t know how… Are you familiar with ray tracing and graphical methods?
Adam: No. Let’s do it.
Andre: Let’s go through this very quickly. So, a ray tracer is a way of rendering 3D scenes, where you put a point in space and you have a set of objects in the same space. And from this main space, you will project lines as if they were photons, like particle of lights and see how they behave in this 3D space filled with objects. And the goal is to, by emulating trajectory of photons. Emulate the way light bounces off objects to go from, for example, the surface of a table to the surface of the wall, to the eye of the camera or the viewer.
And that’s a rendering technique that is quite useful for reflections, for example, because as you can see it’s really natural. You project your points somewhere, if there’s an object that intersect this projection, you can just bounce off it and then keep going until you do 13 or 15 bounces. And then take the color value of this ray of light. And this will give you one color, one pixel on your screen. So that’s basic ray tracing.
A ray tracer can be seen as basically a function from, as I said, a set of objects and its starting point, like the position of the camera in this space. And it gives you a 2D image. So it’s a function from a space, a set of object, a camera to an array, a 2D array. And since you can see it as a pure function, you can implement it using mostly pure function. You don’t have to state. You can go very easily and very naturally towards very basically in your algebra. And that makes Rust very… It doesn’t make Rust shine, it doesn’t make the features of Rust shine because you can write everything as, you do a copy instead of referencing and mutate objects.
So that’s my experience with Rust is basically writing pure functions and writing it just like Swift, so you copy everything and you never reference anything. So, unfortunately I cannot tell you much about how different it is from Rust. I know that Rust has the boring mechanic that is extremely useful for this exact purpose that is referencing stuff, passing references along and making sure you don’t reference something that is already borrowed by something else in case you mutate it and break this assumption that your reference is safe where it’s actually not because it’s been mutated by something else. But unfortunately, I don’t have programming experience with it.
Adam: One of the features that makes Rust exciting is this way of that you could share data across threads for instance but-
Andre: [crosstalk 00:11:43].
Adam: …if everything’s immutable, then there’s no advantage there.
Andre: Exactly.
Adam: So back to Swift, how are nulls handled in Swift?
Andre: So the goal of Swift when it came out was, as they said to do Objective-C without a C, which meant to learn from the mistakes of previous programming languages. I say mistake but people would say features. What I really mean is, let’s make a decision about what kind of bugs we allow in our language and they decided that null pointers were not a acceptable bug to have in this day and age. And what they did is implement what we can see in languages like Haskell or Scala, where you use algebraic data type called maybe or optional in Swift, which has two possible values or two constructors. It has either none or nothing or nil or it has a sum constructor that holds a value, arbitrary value of any type.
And Swift does not have no pointers. It has some magic behind the scene to be smart about what is a no pointer, what is not, and represent them as nil. But really what you interact with is this algebraic data type that is either something which is wrapped into this type or this nil constructor that has no information about it. And the goal of this is to eliminate the bug of referencing something that doesn’t exist and using it even if it doesn’t exist. It makes the compiler able to really easily tell that you’re making a mistake when you’re referencing something that can be gone from your control. So, for example, typically in iOS developments, you have a label on the screen, and you’re not responsible for instantiating this label. Something else will at some point, but you don’t know when, you don’t know where, you don’t know at which point it will happen. And maybe that when you’re trying to use it, it’s not there yet, or it’s gone. And the way it’s represented, it’s using optional.
So, this label is either there, so wrapped in a some label or it’s gone or not there yet and it’s a value of nil. And if you’re trying to use it directly, the compiler will tell you, you cannot use it directly because you cannot prove that it’s instantiated yet. You have to do some case analysis to say, “Is it there? If it’s there, I can use it and it will do this. And if it’s not there, I will do something else.” Either ignore it, or maybe do the instantiation, and then use it. Or maybe you do something else. For example, it’s an error or it’s a huge mistake, so I should move to some other view or display an alert that will say, “This has been wrong because it was supposed to come from the server and it’s hasn’t come back, therefore something’s wrong with the server.” And that makes the whole category of bug disappear because the compiler will always tell you, this might not be there and therefore you have to handle the case where it’s not there.
And you contrast this with, I was using the Java example but we’ll keep using it. Java has those nil references or nil pointers expressed as null which are not different in the type of system from regular references. If you have an object and you have a reference to the subject, well, maybe it’s null maybe it’s not, but you don’t know. And the compiler doesn’t tell you. You could use an optional type in Java. And we are seeing more and more of them with libraries like Guava or more recently I think it was Java 8 introduced the option type, where you can use option types in order to bypass this problem of not knowing if it’s nil or not.
But since you don’t know, at no point you can be sure that, either you are dealing with the null references or you have to deal with the null references. Or if you’re dealing with it if it makes sense because for example, you just instantiate an object and you use it three lines later. Technically could be null, but there is no reason to believe it’s null because you can see it. The problem gets worse when you for example, leave the code evolve for a long time and you have multiple lines going through those two points. Even some functions are called and some mutation happens. And then really it becomes much harder to know if this reference is still valid or not. And that’s what Swift does to eliminate this problem. Is make it a data type.
Adam: So this ties into the topic of totality?
Andre: Yes.
Adam: I believe Swift cannot enforce totality, however if you have an option type or any I guess, some type and when you deal with it, you handle all the possible cases. Then Swift is allowing you to write in a total style.
Andre: Yeah, exactly. It really helps to have a compiler that can tell you whenever you’re forgetting something that you really shouldn’t. It also has this extremely nice auto complete for switching over algebraic data types. So if you write your own algebraic data type that is not optional, even a complex one, it will automatically generate for example, a switch case to do case analysis on it and not forget any cases, which is interestingly enough better than the default GHC option when you’re using Haskell because for example, in Haskell if you pattern match on a data type, if you forget a case, it will compile just fine and explode at run time if you hit this case. That’s also unfortunate and that’s also not total. And that’s one way where Swift is enforcing “Accidentally” totality by making sure that you handle all possible cases at all times and not forgetting any one of them.
Adam: You mentioned the halting problem. Are you comfortable explaining what that is? Briefly or…
Andre: Basically what it says is, you are given an arbitrary program. It could be anything, it could be literally anything. Can you tell if this program can terminate? And if so, will it terminate in a good state or a bad states? Or, are there inputs for which it will not terminate or are there input for which it will terminate? All those questions are corollary to the halting problem but the original is, can you tell if it terminates at all? And Turing has this very nice proofs using Turing machines where programs are defined using Turing machine.
So, a program is a Turing machine and the question is, does it exist? Is it possible to make a Turing machine such that if you feed it another Turing machine, the original Turing machine will tell you if the machine that was fed terminates or not. So it’s the same thing as rephrasing given an arbitrary program, can you write another program that can decide if any program terminates or not? And the proof is surprisingly simple, but a bit contrary, if not used to proofs by contradiction.
Basically, you assume that such a Turing machine exists. And by assuming that such a Turing machine exists, you can do some new trick like feeding it to itself and realize that it cannot tell if it self-terminates or not. And that’s pretty funny, right?
Adam: Yeah.
Andre: The problem itself. And that makes it so, you can give up on writing anything that can arbitrarily decide termination of anything. But it does not tell you that it does not exists a program or a class of programs that terminate. And that’s what we’re betting on with languages like Idris and Agda is that, we know there exists some structures that always terminate. So for example, if you have a function like map on lists, you can pretty easily prove that it always terminates by saying that if you take the definition of a list it’s two constructors, either nothing or the tail of the list, the last element, sorry the last [inaudible 00:20:55] element or it’s a concatenation between a head and another list. So the empty list is just the first constructor, the sub one element is the head and the empty list. The sub two element is, a head and list which contains one element, et cetera. And by doing case analysis on this contractor you can say, “Well, if it’s empty, then you return the empty lists when you map across it.”
If it’s not empty, you have the constructor which has the head and the tail. You should take care of the head apply the function on the head and concatenate this result with the recursive call of map on the tail of the list using the same function. What you just did is, defined a recursive call on a constructor that is smaller than the constructor that you were given to begin with, right? Because since you [inaudible 00:21:53] the cons case, the list that is inside the cons case is by definition one smaller than the list that you were given in argument. And since you’re doing recursive calls, you cannot prove that arbitrary recursive of calls always terminate, but you can prove that if you make recursive calls on constructor that are always smaller, they converge toward a base case, which is our empty list. And that’s one structure that we know always terminates. If you have a function or a program that makes self-recursive calls using constructor that are always smaller because you were able to restructure them using case analysis, then this function will always terminate. And that’s how Idris does for some cases.
Adam: So, because a recursive call and induction are kind of the same thing, right?
Andre: Exactly. Hello?
Adam: Yeah. Sorry about this. We’re having some technical difficulties.
Andre: Yes, you can adjust technology when it’s not to total.
Adam: Exactly. So at it’s root, in a very simple fashion, a function being total means of all of the possible input that come into this, we have to handle all of them. Is that how you would characterize it?
Andre: It’s one aspect of it, yes. It’s probably the most important one when we’re dealing with programming because we rarely write programs that go forever accidentally. Unless we make, as I said, either a very trivial mistake like [inaudible 00:23:35] or a very complex one with multiple, like I said, function calling each other. That’s the case we see most often when programming nowadays is, yes, you have to handle all the cases, not ignore any of them and make calls to other functions that are always also total because otherwise you cannot prove that your function is total if you’re calling something else that is not.
Adam: In the mathematical sense, divide by zero is an interesting case. If you have a function that takes all integers and then divides them. Well, it takes two numbers and divides one by the other. There is a case where it’s not total, it’s not defined when you divide by zero.
Andre: Math cheats because you can always say that… So what you described is called none, very not original way of calling it but, it’s partial function. So, if it’s not a total function, it’s a partial function. Why is it partial? Because only a subset of all the possible arguments can give a result. So, the domain is partial. There is only parts of it that work, but you can cheat saying, “Well, if it’s partial, I can just say that my function is total by saying that the domain is the same as before, except the values that don’t work.”
So divided by, you could say is total if you say, the domain of divide by is everything but zero. And that’s how you would do it for example, in Idris you would say, “Oh, I have a function divide by.” It takes another natural number and it takes a proof that the first argument is not zero. Sorry, the second argument is not zero. And by giving this extra argument as a proof, what you do is that you constrain the domain without changing the input, output type.
Adam: Yeah this type of number that doesn’t contain zero is something you might not find, I guess, outside of Idris or Agda or something?
Andre: Interestingly enough, I’ve posted a tweet, it could be two days ago, where I had a very similar problem where I had to use a function that is of at least one element. It has to have at least one element and such lists have nice properties. One of them is, if you take the head of the list, you will always get an element, right? There is no case where you have a list of at least one element or you don’t have a head because, well, if it’s the cons, you take the head and if it’s the base case, it still has one element in it. Therefore, you just extract it and there you go and-
Adam: The head is total.
Andre: Yes, head is total. Well, the signature list of A to A, is total. You can trust it. It will always work if given that your list is not empty. Now in Swift, there is no way of writing this in a very simple way. So in Idris you’ll just say my list, it happens that it’s a vector but the number of element here is successor of N where N is a number. And that means that if N is zero, then your list is a size successor of zero so it’s one. If N is more than zero, for example four, it means that your list is of size five. And you realize quickly that, well, you have all the possible numbers except zero. You can have all the possible lists except zero by writing down this type.
And it’s very easy to write down this type and it’s very easy to handle the proof, because you can just say, “I’ll figure this out because I used this constructor before therefore it has to be not zero. Therefore, this function can be called at this time.” And Idris makes it easy. But in Swift, there is no way to write this function signature down. So what you have to do is to write down a data type that is just lists. So you have to write, in a none empty list of elements is either something or cons and then just rewrite the whole definition of lists. And that’s annoying, right? Because you have to… It’s fine, right? Because Swift has protocols and protocol extensions.
So you can just give it the sequence protocol and you get map, flatMap, filter drop. That’s a trial for free, but still, mine only was 50 or 60 lines of code that you have to have somewhere and your code base will call a library for this. Or it’s also 50 lines that can contain a bug in it. I don’t know, for example, your reverse. My first implementation, the constructor, took an array and returned an option of an empty list because the array might be empty. If the array is empty, then there is no list to construct, then you returned nil. If it’s not empty, then you return some non-empty list, which makes sense, right? But the way I constructed the lists was reversed. And this is not something Swift can tell you. And this is dangerous, right? Because you get into a situation where you want to express some things, but the type system is not good enough. Or the compiler does not give you enough guarantees about what you’re interested in. And therefore you make very unfortunate mistakes that you could avoid with a different type system.
Adam: An interesting example you brought to mind is, moving beyond head, if you wanted to get the Nth element of a list. So say you want to get the fifth element.
Andre: If you want it to be total in the sense that you don’t want to crash when you access the Nth element, you realize it’s not there is, you have to return a data type like option, or even results and say, in case it’s not there, in case I overflow the array, or I overflow the lists then I return the special value that indicates that you overran the length of the list. And that’s what option is very useful for in Swift because those cases, they happen very often and there is nothing you can do to prevent them, partly because of the type system.
Now, I feel like it sounds like I’m a bit talking about Swift type system because I’m saying, oh, it’s so inferior to Idris’s type system because you can, in Idris for example, you could say the function take Nth takes a list. But it also takes a proof that the list is of size at list N and then you’re safe because the only way to call this function is to both have the list and the proof that it’s of a certain length. And then if you try to make a call where you don’t have the proof of the size of the length, the code will not compile and will tell you, I can approve that N is at least this size, therefore, this function does not type check because I’m missing an argument.
And it’s really useful, it really helps, but in day-to-day programming, it’s really a very nice step towards better programming to at least have optionals in Swift. I think it’s a very good step for programming with just Swift which merge both performance and low-level code and high-level obstruction like algebraic data types, protocol extensions, protocols in general, unions, et cetera. So, Swift has all this machinery to work with optionals, and it’s very useful to achieve totality, even if it doesn’t have all the proof mechanism that Idris has.
Adam: Very true. You mentioned protocol extensions, what are protocol extensions?
Andre: So, some people who are familiar with Haskell or Scala will be very happy to know that Swift has enough tools to have some way of implementing type classes where you can say this type has those properties and therefore whatever type that confirms to those properties have those other functions. It means that you can write, for example, generate operators, for example, map, filter or flatMap on things like new data types that you create yourself.
It’s a bad example because it doesn’t have all types, so you cannot actually define map and flatMap generally. But what you can do, for example, what I very often do is that I have a file somewhere called algebraic where I have monoid semigroup defined somewhere with, what is it called? The plus operator basically, between two values of the same type given a third value of the same type. And that’s already very useful because there are so many types that you can write yourself that need this property, but they don’t have it by default. So if you can just define a couple of things on this type, do a protocol extension saying, “I have this type, it comes from somewhere, but it conforms to monoid.” Then you get the plus operation, and all the goodies for free and that’s very nice.
That’s also what happens with… For example, I mentioned the non-empty data type. You can even conform it to sequence by a protocol extension. And that gives you map, and flatMap and filter. It’s not the monadic flatMap et cetera, but it’s already good enough. That’s really a way to get a lot of functionality for free by conforming to a type that is not a type that you were either aware or existed at the time of the definition of your data type.
Adam: Do you think that Swift should have a higher-kinded types or you think that this…
Andre: So, there is this very funny way of thinking of former language that is… Programming language don’t have features, they just have dreams. So for example, the dream of Rust is to have higher-kinded types. I don’t know what the dream of Swift is, but we should go to Haskell. Like the dream of Haskell is to have dependent types. If you go to Scala, the dream of Scala is… Well, Scala has a bit of everything, but, I guess what they really want is some sort of soundness. I know they have problems now with soundness, given subsumption and higher-kinded types. So you can define programming language by the feature they’re missing. Go is missing everything. Go is missing generics. For example, many people would say, “Oh, Go would be so much better if it had generics”.
So, is higher-kinded types the dream of Swift? Maybe. There are a lot of features that I wish were there. Higher-kinded types is one of them. I don’t see personally myself using them too much. I would have liked to have them this week for example, for one specific case. But I dealt without it and that’s not a feature that I feel really strongly about. Something like dependent types, I think, have much more value because they are allowed to help you in a very strong way. I’m saying that because I’ve also programmed maybe a bit with Idris and I can see how the relationship between the programmer and the compiler changes once you have dependent types.
I know this will never happen and there is no way of making it happen, right? It would be another programming language. Even not be Swift anymore. But I think there’s value into looking into other features that would implement. Try to see if they would work, try to see if they make sense, try to see if they are giving enough value compared to the costs they have. For example, a lot of problems that come with subsumption, when you have subtyping is, you end up with cases, for example in Scala until 2.12 or until Dotty basically.
Where it’s really hard to compute the intersection between two types and you have very complicated cases where the compiler cannot figure out the highest lower bound of two types, and that’s very annoying. You lose a lot of performance, you lose a lot of error reporting. It’s really hard to have nice reporting to detect this cases and say, “I’m the competitor. I accidentally went to infinitely interfere the lowest upper bound and therefore I cannot do it, but this is my best guess. Instead, you get a large page of types upon types, upon types that makes no sense. So adding features to programming languages is nice, higher-kinded type are nice. Now, I don’t know if it makes sense to add them in the Swift compiler given its state, given how useful they are and given how complex it would be to implement them.
There is one thing I would like to say about adding features to Swift is, I would like to have something if there was, for example, a monarchy and I was the monarch of programming languages and I would have to decide the fate of Swift tomorrow, I would say we should have some way of temporarily disabling features. For example, the no check bypass strategy, which is, exclamation mark. I would really like to have a pragma or something that says at the beginning of the file, “This is strictly forbidden, you cannot have this in this file.” And put this somewhere in the recommendation or in the type signature saying, “This function cannot have optional force cast or type cast. You cannot cast types to other types arbitrarily.”
Things like this. Very basic. Removing of features temporarily because you don’t use them, right? Because if you use them either, you really know what you’re doing and therefore it should not be the default. Or if you don’t use them, then you should not be using them at all and be safe and trust your code that it’s not doing some funny thing behind the scenes. Higher-kinded types are a nice dream. I wish I had them. I don’t know if it’s reasonable.
Adam: Could you have a code linter and give it a list of all the partial functions in the standard library and say, “I want my compilations to just fail if I hit one of these ordinates.”
Andre: Yeah. What we do where I work right now is we use this wonderful library made by those wonderful people of the Swift podcast. What is it called? I have it here. Swift Unwrapped. One of them works with SwiftLint. SwiftLint is a linter for Swifts.
Adam: So that takes you towards an approximate total solution where you could ban the use of options?
Andre: Yeah. Unfortunately, there are multiple signs like using null is one of the multiple ways that Swifts makes program total by proxy. There are others, for example, the way you have exceptions rather, the way you don’t have exceptions is very nice, it gives a lot of peace of mind let’s put it that way to think that you can trust every line of code as been executed and not potentially crashing and giving out some huge stack trace that you don’t know where it comes from.
Adam: So let’s explore that. How do exceptions work in Swift?
Andre: There are no traditional exceptions in the sense that they are… For example, if you put your own language like Java, which is a good example because everybody knows it and it has been there for 25 years now. Java has checked and unchecked exceptions. When I talk about exceptions, I usually mean unchecked exceptions. Oh, and Scala has them too. Unchecked exceptions are exceptions that can happen at any time, at any point during your execution. Maybe I just skipped over what are exceptions. I will just do a quick reminder.
So exceptions are what happens when you reach a state that is not acceptable for your program. So if it reaches a state where it’s literally stuck or does not know what to do, or is not supposed to go there because for example, it’s the page fault, it will stop execution and raise an exception. And that is, it will go to the last function that has called it and say, “Hey, something went wrong, please deal with it because I cannot.” And if this function cannot deal with it, it will go to its caller and say, “I don’t know what to do with that, deal with it.”
And it goes that way over and over until it reaches some function that says, “Oh, don’t worry. I know what to do, we’ll just use this other code path because, if that went wrong, it means, I don’t know, for example, the server, network is down. Sorry, the network connection is down, therefore we can use local data.” And this function knows how to deal with it. It captures the exception, resumes execution and goes towards another code path.
So Swift does not have this mechanism where anything can crash at any point. But it does not have checked exception either. So checked exceptions are exceptions that you know they can happen and you know what kind of errors can happen. And in Java it means that, you annotate your function with the type of exception that you can expect. And when you call a function that can throw an exception that is checked you have to catch it and you have to… Sorry about that. You have to take care of all the possible failures that can happen. Since you know what they can be, it’s quite easy to be exhaustive and choose a appropriate code path for every one of them.
Now, it’s not a solution to everything because checked exceptions are quite annoying to deal with, especially when you have multiple of them stacked together or nested. And then it makes dealing with error painful in the sense that you have lots of [inaudible 00:43:23]. And most of the time, you don’t know what to do with the error, because, well, you’re not responsible, if the network goes down, what are you supposed to do? I mean, for example, you’re logging in and the network was down. Well, you can’t log in, I guess. So you just stop or crash or if it’s an assumption that your program makes, if this assumption is broken, then it makes sense to crash. So there is no reason to catch this exception.
So what you will do in the crash block is just throw another exception or just plain crush right there. So it’s not a solution to everything. Swift’s solution to this is to have another annotation that says, “This can throw something but we don’t know what it is.” And it’s a form of checked exception except you could say it’s worse than Java because you don’t know what kind of exception you can expect, well, what kind of errors. But they have nice utility around it. So for example, if you have multiple exceptions or multiple functions that can throw exception, you can bottle them together in a block, and it will all go fine.
You can also do something interesting that is, if you have an exception and you don’t care at all about the error, you can transform this into an optional and say, if it’s an error, just put nil instead. And if it’s nil, I know something went wrong and I know how to deal with nil because I’ve been dealing with nil my whole life with my whole programming in Swift and that’s one way to deal with it.
Behind the scenes there is no stack trace where you unwind an exception. Like I said, notifying your caller over and over again until it’s handled. So it’s not an exception in the traditional sense. It’s closer to an error type because you return something and it happens that what you return is an error, but the syntax is very close to exceptions because you have a try block and a catch block. So, to answer the question, Swift does not have a [inaudible 00:45:32] type. Swift’s exceptions are technically like result types because you return either of two things without unwinding a stack but there is no stack unwinding like traditional exceptions.
Adam: Interesting. So you are an iOS developer, but you clearly have an interest in some more like Idris, Agda. What brings you to those languages?
Andre: So my history with programming is interesting because I’ve like many people started programming making games because video games are very nice. You play with them, you learn with them, you have very good experiences and it’s a way to exhibit your creative impulses. If you want to do something but, for example, you’re not confident in writing or you’re not confident in singing or it’s too hard to learn music and you’re used to video games, you might think, “Oh, when I grow up I’ll just write video games because I love them.”
And that’s what I did. I started writing games and I started working on a game for a long time with a group of people and doing that, I discovered that there are problems that I would like to solve that my programming language cannot solve or if it can, it cannot do it in a way that I would like to do it. It cannot express the things I would like to express.
So I discovered languages like Scala and Haskell. And was very happy with them for a while until I discovered that, again, they have some things that I would like to express that they don’t allow me to express and with a bit of time and a lot of work, I discovered that there exists programming languages that allow me to do this and they are theorem provers like Coq. And I tried Coq for a bit, but it’s not ever going to make for programming actual programs, right? You wouldn’t write games in Coq, you could. I don’t recommend it.
And then I discovered Idris as a programming language with dependent types, which has all the nice things I like. Like the Haskell syntax, dependent types and its ability to express formal properties, mathematical properties about your program like simple proofs and more complex proofs. And it’s a way of writing proofs also that I really enjoy because it’s very hands-on. Some people will say that it’s barbaric because you write your case analysis in a way that is not automated.
If you know about Coq, you know about the tactic system and the tactic system allows you to write proofs in a way that is extremely expressive and extremely simple and automated in a way that allows you to extend your proofs very easily. And if you do it in Agda or Idris, if you try to change something in your proofs, you will have to change a whole bunch of stuff. So, it’s not very useful. It was useful, but it’s not very ergonomic for a couple of things, but it allows me to express some problems that I would like to solve. And I said this in 30 seconds, this evolution took, I don’t know, 10 years to go from basic making games to looking at dependent types and type theory and category theory and actual algebra.
It’s a huge learning curve. But I think it’s worth going through because you really learn to recognize patterns, to write code that tries for those algebraic properties. And once you realize that you can use those algebraic properties, you can write code, or you can make architectures that don’t have to be so complex and can use things like type classes to generate code that you would not have to write and code that you don’t write is code that is trivially correct. And that makes your code base nicer and that makes your maintenance nicer and then it makes your day easier, et cetera, et cetera.
So, I think that is very large value in learning more formal programming language, more formal ideas, more theoretical subjects like algebra when you’re a programmer because you can use this knowledge, maybe not directly but it trains your brain to detect patterns and apply them where it’s useful. And it’s also a very nice community and very nice field of research.
Adam: I’m glad that you were able to take learnings from a more abstract area and that they help you in your day to day. So, if everybody, all of a sudden had knowledge of all this information and we all were writing in a total style, what would software development look like?
Andre: It would be very slow. It would be very, very slow. It’s already really slow as is. One huge drawback of writing in a total style is that, lots of stuff that you don’t care about has to be handled. And most software nowadays, don’t care about those details. So you would waste a bunch of time defining or proving properties about your architecture, your data types, that really are not interesting for the end product.
We have lots of cases where you use technology and it has some unexpected behavior. Like you have an application, you try to launch it and then it freezes or it’s just slow or the input on your screen does not work as expected. Some tiny things that are a bit annoying. Like you connect your Bluetooth speaker and it takes a while and then it doesn’t connect. And then you turn it off and you turn it on again and since you’ve reset the state, it’s back into its initial state and therefore the state transitions are much more predictable and then it goes to the correct state where it connects.
All those are tiny problems that could be very easily solved if we had better way of checking for those state transitions. And right now we don’t really have ways of dealing with state transitions. We can write pure functions, very humbling, Haskell, and deal with state but we cannot prove that all our state transitions are correct or make sense. And that’s one thing that dependent types allow you to express is if I have a state transition from A to B, it is not possible to call this function with something else than A, therefore I will always go to B. Therefore, there is no crash between A and B.
Adam: Yeah. I hope we get there. I think the dependent types will start appearing in places. At least that’s my hope. It’ll let us encode these concepts and have them verified at compile time. So I want to be conscious of your time. I think we’ve already gone over. Thanks so much for talking to me Andre. It’s been great.
Andre: It’s been great to talking to you too.
Adam: So that was the interview. If you liked this episode, do me a huge favor and think about who else might like it and share it with them. For me sharing a tech podcast that I like just means, sharing it in my company’s Slack group. There’s a off topic channel and I just throw it in there. So if it’s the same that you work, yeah, share it out. Right now the main thing I’m trying to do is just grow the podcast listenership. Until next time, thank you so much for listening.
Sticher
Overcast
Nov 04, 2024
52
min