SBTB 2015: Paul Phillips, Suffuse: Usable Virtual Filesystems
Recording: SBTB 2015: Paul Phillips, Suffuse: Usable Virtual Filesystems
hi hi so you didn't mention it but I used to work on the compiler a lot not anymore so here i am to talk about my thing that isn't the compiler which is sort of you know really vaguely related to scala frankly nobody would invite me to talk at these scala things that I weren't coasting on the past and the fortunately the invitations are trickling away so but in the meantime I'll abuse them to talk about things that have little to do with scala accepted in terms of you could use scala on top of them like this one virtual file systems so you all saw the advertisement i guess that's why you're here I I don't even know if what I'm talking about is actually what's in there probably not it's but this is better so you know go with this yeah I I keep giving talks about this and I guess I think that they're too unfocused because the idea is like so good and so big there's too much I want to hit so I decided with this one to go really narrow and just talk about type files which is this kind of nonsensical seeming notion which is actually awesome so here we go typed files just think that Wow typed files what does that mean so we live with file systems right now that are effectively typed file systems with one type I mean they're like dynamic languages their unit typed every file is the same it's got a bunch of stuff in it what's in it well you might have some hints you might have a file extension you might have you know the resource fork you might just have a convention it's you know you might look at the first few bites and see a bomb or XML thingy whatever but all these things none of these things actually enforce anything about the file they're all like yer istics you apply to try to figure out what's in there and then you hope and then if it's really important you actually have to inspect every bite and make sure and then as soon as there's one more right to that file your entire inspection goes out the window once again it's anything who knows this is crazy way to live create there's no reason to do it we don't have to do it so let me define some things data is just bites that we don't know anything about a value is bytes that have a type so it's data we do know something about something that we know to be true it has some form it has some meaning whatever it's something other than raw bytes and a type which can be defined a bunch of different ways and is but for our purposes the type is a set of possible values for a blob of data and that doesn't necessarily mean we can enumerate them it just means that we can recognize it so really at its at its most simple and least elaborated a bite a type is a membership function does this pile of bytes actually meet some tests that's important to me to say that it's a thingy yes or no and as long as I can ask that and get a consistent answer then I have a type importantly a type specifies all the possible values not the like just most and we'll check at runtime and see if anything else snuck in there the notion that there is such a thing as a dynamic type is to me like very wrongheaded they're using the wrong nomenclature types are static properties they're not things you check later it's not and you know this is not an inspection let's just make sure thou'rt of thing it's a it's a thing that's true it's a formalism it's you either know or you don't these are very boolean notions so yeah and if you have to if you have to check it's not a type all right so how might we define types and I'm not really talking about tight files here yet but of course since you know where we're headed you can sort of look at some of these things in that way because that is where we're headed so the like the very minimal form is as already mentioned just a predicate something we can ask an Oracle as it were not the you know not that lawsuit happy you can kind but the kind that answers questions and so that's the minimal version but we need for efficiency and am sanity we need something much better than that we need well we'd like to be able to produce values of that type that's much more useful than just need a little recognized values of that type and that's normally the way we do it we have what we call constructors and constructors usually work on other types and then there's some mechanism by which you can unroll things all the way down to something primitive where we have types like int or whatever where you're just going to take some 32 bits and interpret it to have some meaning that it's a you know a signed integer between a min value and it max value whatever point is you're just going to at some point you're going to just ascribe meaning to some bits and then every other sort of thing is the composition of some previously ascribed meetings for some bits but we're missing like a huge piece of the puzzle when we do things this way because what's really important in almost everything is not how to build things from scratch but how to change them everything about programming is the incremental change of systems especially the bigger they get the more important it is and we throw away really important information when we don't think in terms of change we say like well I have an a and then later I have a B but that's not enough information we want to know when we have an a if whether the thing we're trying to do to an a to get a B is itself acceptable and that's not something that we can necessarily know by looking at a and B individually so there's two things going on here there's not just the virtual files there's change orientation is sort of the unifying notion of like all the good ideas that I have that I can't do in Scala or anywhere else for that matter so change d is undefined there and it's going to be undefined everywhere but for some future talk it's some type specific notion of how it is that it can be changed notice that it actually depends on the values you can constrain the set of possible changes based on the value a complex system that works is invariably found to evolved from a simple system that worked like so true anybody who has spent any amount of time in this business has had to go back and rewrite something simple because they wasted half their life trying to push some complex thing into working no comments from me 3500 commits into Scala see so the like nothing nothing makes makes me warmer on the inside than the notion of a simple thing that works continuing to work and what's really at the heart of this though is is change the reason you can say a thing like that is that it matters how you get somewhere right there's a huge difference between a system that is just dropped on you as is and somebody says now make it do this and one with a very clean series of changes to a very simple beginning that got where it is I mean a huge difference these are night and day and yet we act like they're the same and like it only matters you know what sort of changes we're going to make to it but its whole identity is actually wrapped up in how I got here so we have these constructor oriented languages pretty much universally but we could limit construction to really simple things and then make you change things to get where you want to go and buy controlling change instead of trying to control construction we can enforce more interesting things than we can enforce in values alone I hope my next slide is what oh yeah it is okay so there was my little first example there I have a couple of tuples three o'clock exactly 75 miles per hour three o'clock and one second zero miles per hour now either of these is fine in isolation there's no way to look at one of those and say that's an unacceptable state however the change from the first to the second is highly unacceptable that's what it looks like when you crash into a wall at 75 miles per hour this is a material difference right i mean like it should be obvious here but this kind of example is everywhere if you think about it and it's not just about the things you can rule out it's the errors that become extremely obvious when you see things in terms of what change just took place rather than two distinct things is this okay is this okay we can't look at them individually we have to look at what we're doing so we constrain instead of the set of possible values the set of possible derivations in other words the set of possible histories of a particular value so if we want to say with a straight face that we have typed files then there's no sort of like retrofit we can do where we're like yeah man it's really it's typed and if you can change it in such a way that it stops having whatever invariant we associate with a type then it's not a type filed has to be always that like we we don't let our programming languages to say like it's a string probably unless somebody did this or that I mean it's a string it has to be it always is same with a file and we can do this this is what part of what small part but a really important fundamental infrastructure sort of oriented part of my idea and here's how we do it before we can do that though we need an intermediate step in that is to have immutable files which sounds kind of nuts except that we use immutable files all day long probably everybody here uses the same system for immutable files what's that yeah and get in particular right version control in general and get in particular which is impossible to avoid even if you don't like it but but get is really just a nothing more than an immutable file system something that is just a very straightforward here's a hash here's some data and now if you want to change it I'll give you a different hash and I'll keep track of that and the change and I'll just have a bunch of changes all lined up well great that's just what we need for what I'm describing so that's just the kind of thing will integrate into a virtual file system so every time you write to something you actually are going to be doing a git commit maybe you're going to be trying to do a git commit but you're also going to be up against enforcement of the type of the file what is the type of a file what's that mean well we have a huge range of possibilities here but there's really simple ones that we would like things like my text files should end with it like not have like a partial line at the end with no new line right you see you see all these sort of like ad hoc attempts to sort of retrofit that sort of thing I just just make it true always don't let it not be true or i mean there's any number of sort of like bashed level or source code level or just sort of code sanity level you could even have you know the formatting be part of the type there's literally anything you can think of can be part of the type because all that you're doing here is writing an acceptance function for a change to the file so that when somebody tries to do something to it then either it's still true in which case we can commit it or we know of a way to make it true in which case we can do that and then commit it or it isn't true in which case we won't commit it and therefore sanity is preserved across all rights and we can expose everything interesting about files in the metadata through extended file attributes so if a file has a type in the sense that a person said this file has this type will expose that in the metadata if it as a type in the sense that we looked at it and said it probably has this type like it's called foo mp3 and has audio data in it I mean we can easily infer that to be an mp3 file but that's still different than the user saying like I know this is an mp3 file so we expose that in the metadata and if we have no idea what it is we'll expose that in the metadata but point is all of our these this rich information about what's inside of files is all stuff that will expose in a way that's easily accessible by tools so there's this persistent analogy that works really well compile-time runtime program has compile-time types of the things that we check at compile-time then we run it and then things happen well there's kind of a compile time for files and a run time for files compile time is when you try to change it and run time is when you need it run time is when you need it to have like you know some some things needs to be true about it so right now we effectively defer every such integrity check to the time when you need it and I'm saying we can do it when we change it so that we already know without having to the consumer doesn't have to be like okay now let's double-check the truth of whether this is that or just crash horribly if it's not if it says it's an XML file it should be an XML file you can know it 100% there's no reason to have any doubt about that and it's easy to enforce just by never committing a change to an XML file that doesn't produce another XML file and that's a syntactic constraint that's easy you could also have arbitrarily complicated semantic constraints if it's like a maven pom file then whatever the hell I mean I don't have a clue but I bet there's a whole bunch of constraints some known some unknown unknown to man or B or computer program but still we could we can fare these things out eventually the there are constraints though about how those things evolve and it would be easy to actually have like sensibility constraints like your version numbers shouldn't suddenly drop by 10 right like this is why I looking at changes is relevant if your version not like the version that you produce should increase monotonically you can enforce that in the file not commit right like you can actually have a check against these kinds of sanity things that you're completely at the dependent of people right now doing their process correctly these things can be codified and capsulated and use like clubs so anybody who stopped right there would think to themselves well that guy's going to have some real problems when something happens like some very sensible right is broken by the operating system into two rights and so you get a half right and then like it's not right and everything blows because fortunately we have this nice buffer zone if you try to do a right to a file that is not type correct in the sense that it conforms to the defined acceptable set of changes then it does not get committed but it doesn't get thrown away it's still there it's in the it's dirties the get index so we have this virtual git repository and now we have a virtual dirty git repository so those of us that are looking at the files in a direct way which is all of us all the time right now since we lack this system would see the change but most of our code that runs in general the code we're not actively developing or otherwise needs to do things like see this change is looking at the repository itself directly it's working from a virtual file system that doesn't see any dirty changes it just sees what's in the repo so it's invisible those that that code never sees it and when later another right comes along and fixes it and it is type correct change then it gets committed and then it's seen so all this code all of our code all the time can actually assume things about its inputs and these things that it assumes can be arbitrarily interesting like far more interesting than you can write in in any programming language I'm aware of and that's pretty powerful stuff is because you actually have a lot of room here for like time consuming type checking for that you know you wouldn't necessarily want to take five minutes to do it but you kind of could because you're into the user is really insulated from it this is all kind of happening asynchronously and it either gets committed or it doesn't but you can just proceed with your life like it's all getting committed if you want so we have these multiple views and they're you know I've only described two there could be more there's like various scenarios one can imagine you can have like there can be middle grounds between good and bad like probably good or sketchy or you know who knows right like it just depends on your system but the opportunity is here for arbitrarily you know complicating the different views of the world the important one though is that is the central one the one where everything is always properly typed and everything else is just like how much room do we want to give ourselves to wiggle type source code so here's where we get into some actual Scala so that's why I knows what you came for you're dying for this so we're going to have typed Scala code but we're going to mean this a little differently right we're not talking about types in the internal compiler model we're talking about the taught the file itself the source file is it well typed from our point of view and our point of view is not the knot is going to be different it's actually a subset of the same idea which is to say it's well type Scala code from our point of view if we can parse it and get through the namer phase which is to say assign symbols bind the names and so then we will store all that information and now will only allow changes that retain that property so you can't actually make your scholar code not parse ever again right there's no way to unhone that doesn't parse not in the repository because that's not well typed and now every change that we make to our source code that's well typed in the sense of in our sense not in their sense is a change in the repository that lets us see how our code is evolving in terms of the AST because that's guaranteed to be available since that's the point that's how far we're typing our source files and let's see what that can be an example was all right so this is the kind of bug I've seen many many many many many times and it's kind of like these 75 miles an hour zero miles an hour thing in the sense that each of these programs individually short of a like a I level analysis it looks plausible of course you may be a pretty bad variable name or for either of these to be plausible but still there's nothing like no a priori way to say like one of these is definitely wrong but the change from one to the other is the kind of change that's almost always wrong can we see what the bug is here yeah so we're shadowing we have a back-up sim they're ready to fall through into our scope now we changed the name of an invariable and we miss one but it still compiles because it falls through from above this is never correct even if this was what you meant you're a jerk for ever having code that you could like where this could have been correct you're still wrong this change can't possibly be decomposed into a sensible series of changes it's wrong but you cannot see that unless you're looking at it from the point of view of the change and not from the point of view of source file here comes source file again and that's the kind of thing that we're after here change orientation so it isn't just that we can enforce type correctness of each of those which we can it's that the errors that we issue our that is an automatic error for us the narrow the Scala see can never give in its batch mode so now things get really interesting so our system is loaded with type files many of them will have a type as simple as like sequence of lines of text right it'll just be like it's it's utf-8 it has lines of utf-8 but even that is very useful all by itself if we're going to maintain that invariant it's actually easy when you're just writing random bytes to a file to screw it up and make it vet invalid you TFA that's bad shouldn't allow that we don't have to allow that but more interestingly at the shell level and from the interactive standpoint if we have these typed lines or you know that maybe lines or maybe something even more interesting than we know a bunch about the individual elements and we have typed pipelines so we can act on not on lines of text but on tees whatever a tee is and furthermore everything that we know about a tee can feed into the shells so that we can get things like completion on all the names of the fields of the thing that is a tee so the example here on the third line which says cat some comma separated value thing and then goes into a filter and then it goes underscore den and so presumably the first line of that CSV was the names of the columns one of which was like name and then Here I am typing an end tab which completes to name because it can it knows perfectly well exactly what's in that CSV file and what the names of the columns are so and then for that matter now it knows that those are strings and so I can know it can work on strings at this point we can get like the kind of completion on the command line that's available in IDEs better in many ways and all we need is to have like expose this information and maintain it which is trivially achieved in the hypothetical not existing system I'm describing trivially achieved that's right and then of course you know like we have there's this crazy series of 50 years of accumulated hacks and things like find an LS and whatever to you know chomp through these like single bits of data and figure out what they mean and it's it's crazy it's nuts right I mean we we can have like a complete attribute map associated with any file which is to say typed metadata right like meaningfully typed metadata you can have a thing called size it actually as a size and isn't just some random int that's overloaded to mean the length of the string for the target of a symbolic link or the length of a file for a file or the number of references for a directory plus two I mean it's pretty it's pretty nuts all of this can just be this is Gordian knot territory that all of us can be redone in a vastly simpler fashion some of it would still have to run on that infrastructure but from the user standpoint we can have find grep type tools that are just a million times smarter and have a tenth of the options and one of the great things that anybody uses a typed language especially scala knows is the great advantage of types for filling in the gaps in your thing so you need an a and you have a B but it knows the relationship between b's and a's and it can just make your bna that's really handy it's a lifesaver in many many cases in fact I mean it's not just implicit conversions but implicit in general or just ways of setting up logic to how you like step in and say like this is how I want things to work when you reach this point where you've got this kind of a and this kind of be this is how that works well we can push that really far we know how to convert between every imaginable kind of audio video image we know all this stuff you need like three programs ffmpeg and you know whatever the equivalent is and a couple others so literally from that point forward never again do you have to be like oh I've got a you know a wave and I need a you know AAC who cares man why is this much busywork inflicted on people we know how to do it we should just say hey computer this is how it happens and then when you need and wave and you give it an mp3 it's just like okay man I'm just going to make that into a wave now clearly there are like you know interesting questions here how to deal with like lossy versus lossless and expense and caching and lalala but you know what all those questions exist in the busywork version 2 plus you have the busy work so I think you're much better off actually having an opportunity to define it in one place say this is how it works come bug me if you're confused I'm going back to doing some actual logic and not busy work for you computer that's my last slide I'll take questions hold your applause please we'll have a nice rowdy one later oh yeah absolutely well I mean I so a by sequence sequence is kind of a wrongly leading term I actually want to say decomposable so we're really looking at like something more like the pattern calculus where things are either atomic or composite and and each element is either the next you know it's it's either decomposable into two elements of unknown decomposition or its atomic so yes you you can walk a tree that way you know you can decompose anything that way that's intentional I knew there'd be some jerk that took that example and pointed out how bad it was okay I wrote that like 20 minutes ago i'm like this I'm writing I'm like this is the worst okay true but on the other hand it's good in the sense that it point like that it brings up that question because like this stuff is all at the boundary yes for sure you have to define like if you want to avoid sort of pathological behavior you know you're not just going to say just do whatever conversion feels good computer it's no problem right I mean you don't want it like just turning every single mp3 and do a full into a bad black just because you happen to ask for some flax or something right yeah I I think you end up defining like a sort of you need you need an abstraction that folds over all your audio data really right and so like and then of course there's you know there's like some stuff that you can sort of universally have and it's not much and it's the classic sort of look at my cross-platform toolkit and how much it sucks right because I've managed to do the three things you can do on every platform but that said like this is totally a solvable and like a distributable problem because one of the great advantages of this approach is that we can crowdsource a great deal of logic right like Indy can have like you know a git repository essentially of type information about files and send pull requests to some sensible person who's like pulling stuff together that is able to make sense of our things and again it's like when you compare it to the status quo it's miles ahead it's easy to see like places where it'll break down if we're stupid about it but presumably we're not right we'll avoid those and get the good parts so I'm sorry yeah so he asks how to distinguish between a good right that comes in two parts versus a bad right that's thrown away so the bad right isn't thrown away the bad right is just essentially buffered you don't distinguish between those you either see a good right which is committed where you see a bad right which isn't followed later by another bad right which turns into a good right on top of the previous bad right which is then committed or you see another bad right which is still not committed so there can be arbitrarily many rights and only when it adds up to a right that's valid is it committed so I'm it does that answer your question so that is where we have to head into multiple universes beyond two that's sort of what I was avoiding when I said like you won because we could also have a reply we could we could commit every right even bad ones and so then we would have a repository of type correct things we would have a repository of pending bad rights and we would have you know dirty and ex maybe or we wouldn't but in that scenario if we commit everything but have a a blessed repository and a not one then it's just a matter of coalescing rights in the one repository in the bad repository and then move and Rover to the good but for simplicity I kind of take the position that in general you that doesn't happen and when it does it's very short term and so for now I assume that like dirty right sort of approach works well so I consider acid to be is the concern of people above me right it's like people want to ask questions about like distributed objects and acid and like all kinds of fascinating stuff and I'm all for it but honestly all of those are like you somehow you managed to build whatever you built now on top of much less reliable files then I'm proposing to give you thus I would say it is like a strict improvement to just say like well I could use these better files to do things on way I'm doing now and anything else is gravy are the types themselves versioned absolutely in fact this is like this change orientation is extremely pervasive so yes it's all it's it's turtle wheels all the way down yes mana gene like how the because it's still only you've moved from like one dimension to two dimension when you stop looking to snap shots and look at the value history but you not need a third dimension effectively which is the value history now intertwined with the changes to the type if any that also occurred over time right so but this is all tractable stuff if one takes a highly change oriented view of the matter so yeah sure version do you got it yeah well that so that at the moment like a type is an interface so it's just some what it you know that the at the very simplest most universal it would be a program that you can run and give it a file input that either return 0 or 1 which is to say either this is a member of that type or not so then we'll have like you know much more sophisticated sort of ways to plug into that but that's the essence of it is something it's again that Oracle is this the right is this valid for this type or no yeah no its you I'm pointing right at you you computer that may have different requirements for these crazy file system plugins since you're moving stuff that used to be an application so well they don't necessarily need to separate themselves we actually are way ahead of the status quo in the question is like you have things with different requirements for maybe the same files on the same system we have a huge opportunity here for like just for a random example you could run like any version of Scala you want out of the same place with just sticking the version into the path because a virtual file is able to analyze you know what the path was and come up with it like you know I have a sim length that is to the latest version of Scala whatever it happens to be that's not something I have to manually update that is always the latest version of Scala because it's logic instead of just being a fixed link symlinks that that are two things other than fixed paths are super crazy powerful like a symlink to a database query or you name it and so because everything's under revision control and because the entire thing is designed around the notion of being able to present a repository commit as the file system from which you work it's really quite trivial to have any number of views of the same data to different applications yeah that turns out to be like the easiest problem now there's always a management problem when you have something like that but I think it's a management problem you have any way sorry I don't I just don't know what time it is i don't ok we're good ok yes oh so I did I might have glossed over that but I did gloss over that so type inference how do you do type inference well it's funny type what type inference is I mean type inference is the same thing that we do by hand right now which is like look at the extension run file on it right you run file on it and it's like looks like you know utf-8 encoded text or whatever it looks like mp3 audio data great so probably you know like on when you first fire up the fuse like you run the file utility on everything in the system and stick it in the metadata that the inferred type is what file says it is right and then you refine from there so now but now your file utility is much stronger because it can actually look at the real metadata and say like it is don't even need to look I don't need to process these 8 gigabytes of image in order to tell you it's a JPEG because I can trust the file system and it says it's a JPEG done right it doesn't like everything is brute force in UNIX essentially on a nun type file system if you run WC on a file and it tells you there's 80 billion words and now you stick a line at the end it's going to just start that over again from scratch but we could have something like has 80 billion words in the type right I mean there's no like there's no no restrictions here on the thing right and then we can actually look at that from the point of view of 80 billion word file plus you know 80 characters a text with nine spaces in it okay so now it's an 80 billion and nine word file that's an acceptable change right I've just moved from the singleton type of 80 billion word files to the singleton type of 80 billion and nine word files but that's okay because they're both within the range of acceptable changes that I've free to find for these large files of interesting words if that gives you any gist other questions Eric look at it now you've basically made this like potentially turing-complete verifier that's going to run you know for every file to said giant attacks purpose for life now by downloading files completely being run by my tech checker which might be to an arbitrary stuff and I really have no way to stop it like I cannot in good conscience even begin to answer this question I yeah I have mousou I've obsessed lately about data and code data in part because I'm very interested in restricted languages because there's no reason to work with like general recursion all the time it's not similarly there's no reason to work with like things that change things all the time right for the most part like I would expect to partition type definitions into you know things that are safe and things that aren't which and almost everything we do should be safe if we had a proper notion of how to separate safe things from unsafe so yes I I acknowledge the existence of this problem i just don't see it as like right in my face yet one can ask a similar question about performance and that i could also just sort of throw my hands up and say well just you wait and we'll see hahaha but yeah I mean they're not they're interesting problems but they're in the big thing is that the status quo is already plenty bad the thing is that these it's all spread out over a million different ad hoc ways that are all vulnerable in the same way as whereas we have an opportunity to actually treat these things uniformly I guess that's probably time one more okay right there your question you knew you guys have you filed out yes yes well I I PFS is a distributed hash table and which is very high on the list of things I want to do with it so that's today I just I went really narrow with what I was talking about but yes in other talks I have talked about distributed hash table which is an IP FS is definitely going and like very interesting like very similar but much overlap yes 80 billion yeah so the question is how that information is represented about like what you know about it so that's you know about extended file attributes the extended file attributes are opportunity for exposing arbitrarily interesting metadata typed metadata actually because they can have types as well right like so it's you know it's typed things all the way down but something like that would essentially be a there would be an attribute if you did X a dirt dash L on the file you'd get some meaningful list of keys which you have some like well-known translation which is defined in this a few specification for but one way or another it'll at worst lead to an Oracle which will tell you whether this change is acceptable alright I guess we will stop there thank you very much everybody now you make clap if you look