From 973f78f6fe4a1142fa7f9cf631611f8ecb549d03 Mon Sep 17 00:00:00 2001 From: Simon Heath Date: Sat, 6 May 2023 15:11:24 -0400 Subject: [PATCH] I have some conclusions on effect types now. --- properties.md | 29 +++++++++++++---------------- 1 file changed, 13 insertions(+), 16 deletions(-) diff --git a/properties.md b/properties.md index 4be4b9b..7553eb0 100644 --- a/properties.md +++ b/properties.md @@ -6,10 +6,9 @@ I got five hours of sleep and spent all day being useless, let's try to throw do I want to be able to mark certain key functions with things like "this always terminates and cannot have an out-of-band error like a panic", to make it easier to verify things about the system without needing to go whole hog with a proof assistant. This comes a bit out of my playing around with OS dev and embedded programming and a bit out of my superficial brushes with DO-178C, MISRA and other safety-critical software certification processes. Basically, you should be able to tell the compiler that a function has a property and the compiler checks it for you. Or maybe you tell the compiler that a function cannot have a property and it makes sure it doesn't do anything that violates that. Properties are sticky: if you have a function that call another function that has the property "this allocates memory", then your function also also has the property that it may allocate memory. - -This makes changing properties a breaking API change, btw. +This makes changing properties a breaking API change, btw. I think the way to handle it is to basically have properties be part of a function's signature. -This really isn't a feature for everyone. Some of the things I have in mind are very fine-grained and restrictive. Thus they should always be opt-in; if you don't say anything about the properties a function has, then the compiler has no comment. The compiler may figure a function's properties out for you and output the result in the API docs, kinda like Rust auto trait impl's. My personal canonical use cases are for embedded controllers for robots that are real-time and fairly complex but also fairly hackable, such as drone flight controllers or CNC machines. I could also see them being used in OS dev, some parts of gamedev, maybe some general-purpose libraries like super-fast deserializers or math utilities. Places where invariants are strict and regressions are bad. +This really isn't a feature for everyone. Some of the things I have in mind are very fine-grained and restrictive. Thus they should always be opt-in; if you don't say anything about the properties a function has, then the compiler has no comment. The compiler may figure a function's properties out for you and output the result in the API docs, kinda like Rust auto trait impl's. My personal canonical use cases are for embedded controllers for robots that are real-time and fairly complex but also fairly hackable, such as drone flight controllers or CNC machines. I could also see them being used in OS dev, some parts of gamedev, maybe some general-purpose libraries like super-fast deserializers or math utilities. Places where invariants are strict and complicated to maintain, and regressions are bad. Rust's `unsafe` is kiiiinda an example of a property, and `const` is kinda getting there too. Const code can only call const functions. Unsafe code can *only* be called by functions that have an unsafe block in them. @@ -19,10 +18,18 @@ Like Rust's borrow checker, some false positives are acceptable as long as there You may be able to *assert* some properties are true or false for functions you write. More on that below. -This also sounds a lot like algebraic effect systems, but so far somewhat more restrictive. Effect systems seem to have control flow as a integral part of them. I don't want any control flow to happen based on properties, just the compiler stopping you from doing something unintentional. - They are also related to capabilities. I think with unforgable marker types and a lot of boilerplate you could implement like 90% of what I want from properties. I just want to streamline the process. +## Sidebar: Algebraic effects + +Some people have read this idea and instantly say "this sounds like algebraic effects". So I have done some research on algebraic effects, at least as far as playing with [Koka](https://koka-lang.github.io/) goes, and algebraic effects seems to actually be two different things. First you have effect *types*, which is indeed more or less what I want out of properties: you put markers on functions and they are "inherited" by any function calling them. Garnet's properties may converge into being identical to effect types or it may not, we will see. Second you have effect *handlers*, which are essentially strongly-typed coroutines: a function can "yield" an effect and control flow travels down the stack to some place where the effect is handled, and then the handler can choose to "resume" it and control flow goes back up the stack to where the effect was yielded and carries on from there. I love coroutines, but Garnet is the wrong language for them, since coroutines need either a sufficiently smart compiler or a runtime that can take apart stack frames and glue them back together. + +That said, there's plenty to learn from Koka and other languages with effects. Koka's effects have some interesting examples like `total`, which says that this function is For Realsies Pure. Garnet's `const` is a little like that in practice but specified differently. Koka also has `ndet` for "non-deterministic"; a hardware RNG fits this bill but now that I think of it, it could also be used for stuff that takes input from a user, the network, or other source that the program has no information about. + +So, some of these properties can imply others as well. For example, `Const` things can't panic, and must always terminate. However, going too deep into that results in a hierarchy of properties, which starts becoming inheritance and subtyping, and I am *really* not sure I want to do that. Hmmmm. It might be inevitable though; you have to be able to compose effects somehow. Koka does this by basically letting you have sets of properties, and defining properties in terms of sets of other ones. This is fine, but I'd prefer not to need it if I can avoid it. Some of these properties also need compiler help to enforce, such as termination checking. Other properties, like "no memory allocation", just need to not call any functions that lack these properties, and for the leaf functions to be annotated correctly. Some, like "performs I/O", may be better handled by passing an I/O capability object around. + +Koka is a good demonstration that properties also have to be polymorphic. For example there's `map(f, seq)`, which has any properties that the function `f` has. Heck. Can you specify an array of function pointers and require it to have only functions with a stack usage <= X? If so it starts looking like a dependent type system and I want to avoid that if I can! + # Properties on functions It's useful to consider whether properties are positive or negative. Do they restrict you from doing something, or allow you to do something? So far my brain says "restrict", so that's what we'll be rolling with here. @@ -47,6 +54,7 @@ Of course, `NoAlloc`. I've actually wanted this for real in my toy OS code, so `IO` is another classic, controlling whether or not a function can touch the filesystem, network, etc. Other systems like Haskell or Agda seem to often use it as a stand-in for side-effects functions in general, I'd maybe prefer to make it a little more fine-grained. (Is memory allocation a side effect? Depends on your view of the world!) The exact boundaries are wobbly though. "This function makes a system call" might or might not be a good place to start thinking about it though. (Memory allocation may or may not make a system call, but usually will.) +You could also do this via capability objects that have to be passed through functions, which is probably a better way to do it. Howwever, you will *always* have to be able to sidestep that for logging code, because ain't nobody got time for that shit. ## Constant stack @@ -78,17 +86,6 @@ Simple termination checking seems easy. No recursion, no complex loops, no block Related to `Terminates`, a bit. Is this useful? Iunno! I'm starting to become slightly uncomfortable with the proliferation of these, and constructing a big complex hierarchy of dependencies seems unhelpful. Finding the correct level of detail will be key. -## Other stuff - -Koka's effects have some other interesting examples. There's `total`, which says that this function is For Realsies Pure. `Const` is a little like that in practice but specified differently. There's `ndet` for "non-deterministic"; a hardware RNG fits this bill but now that I think of it, it could also be used for stuff that takes input from a user, the network, or other source that the program has no information about. - -So, some of these properties can imply others as well. For example, `Const` things can't panic, and must always terminate. However, going too deep into that results in a hierarchy of properties, which starts becoming inheritance and subtyping, and I am *really* not sure I want to do that. Hmmmm. It might be inevitable though; you have to be able to compose effects somehow. - -Oh nooooo, properties also have to be polymorphic. For example there's `map(f, seq)`, which has any properties that the function `f` has. Heck. Can you specify an array of function pointers and require it to have only functions with a stack usage <= X? If so it starts looking like a dependent type system and I want to avoid that if I can! - -So SOME of these properties need compiler help to enforce, such as termination checking. Other properties, like "no memory allocation", just need to not call any functions that lack these properties, and for the leaf functions to be annotated correctly. - -If you allow users to define arbitrary properties, essentially as string names, and compose properties of the style `NoBlocking = NoFileIO + NoMutex` or whatever, then we only *really* need to worry about the things that the compiler must be involved in checking. The rest can be developed organically. # Properties on data -- 2.45.2