Lambda the Ultimate

Its often overlooked, but C of the C99 variety has non-null arrays:
int array[static size] can not be NULL. Sure, not exactly the same
as non-null references, but this trick can still be applied at least
across several functions, largely because of C stupidity with respect
to array/pointer co{erc,nfus}ion.

He caught me once playing online poker during a conference. At first I was embarrassed, but now I think that online poker rooms really demonstrate some of the finest technology available today ;-)

Why not post a book review on Amazon explaining the bad advice you gave?

Ehud has already mentioned Ada. Splint offers not-null annotations for C. Nice explicitly requires nullability to be included in type declarations, and Cyclone offers non-null pointers. There are undoubtedly others I haven't thought of.

Non-null references were previously discussed on LtU here.

FWIW, IntelliJ IDEA does support external nullity annotations, but I don't know of any external annotation files available for common libraries. It sounds like a good idea, but hasn't gotten much uptake in practice.

If the return type of the accessor is maybe (since there's no guarentee that the index corresponds to an element of the vector), then there's no problem, as long as the array is populated with Nothing.

Alternatively, a proof that of all values (whose index is) below the length of the vector being valid in the array, combined with a proof that the accessor only accesses values below the length. Obviously such proofs would be more complicated than type checking single methods.

But you still have to tell the caller of the accesser that the index is out of bounds somehow, so you need either maybe or exceptions or something else.

Raising 'mutable fixed-size array in which all elements less than a given N are readable, and the element at N is writeable' to a primitive would suffice, which at least gives a the option of implementing contiguous vectors or VLists.

Yes, it's the complexity of the proof required that bothers me. I would expect that a maybe value would be cumbersome in practice, as it would force people to write code everywhere to handle what is effectively a bug, not an error, and never raised often in practice. It could raise the feature to the level of annoyance, an issue that static type systems always need to struggle against. And if the code is too easy to write, the non-null-by-default benefit would be lost to a degree, as people may just use maybe everywhere and be damned.

With respect to index out of bounds, I see that as a distinct issue to non-null types, though it's very relevant when trying to prove things about accesses in the array. But there are relatively well-known things that come to mind for that, such as dependent types.

What I found curious about what Tony wrote is how it seems to suggest that non-null was a prior default, and nullability needed to be opted into; whereas, when I consider how to implement non-null practically, it seems less trivial than the alternative.

The Maybe type is an implementation detail that does not need to leak out into the interface. Encounter of Nothing during access essentially is an index error and can be flagged to client code in the same manner. This does not involve any complexity at all.

I understand. Every array[*] would strictly be an array of nullable (aka Maybe) locations, which need to be tested at runtime for non-null, so that a static image of a non-null resizable vector can be presented to the outside world.

* Or at least, every array used by a resizable vector.

Actually this proof is not necessarily hard. For most use cases it can be handled by flow-sensitive dependent types, and for use cases that can't be handled that way using a pretty simple solver, you would probably want to fix the code in any case.

The obvious approach is to request a sample value of the type during array construction and then to fill array with it. Or for fixed size arrays it makes sense to take an initializer function (f : int -> `a) as an argument that fills the mutable array with initial values. This could be also a way to initialize immutable arrays.

"sample value" is just another word for "null", the difference being that it can implement some kind of default behaviour; but let's not kid ourselves, this is simply the Null Object pattern baked in.

Taking an initializer function is similar; a vector implementation needs to implement a policy for over-allocating, so it, rather than the user of the vector, would be choosing the initialization. It could just as easily be parameterized with a sample value.

This approach (null object pattern) ameliorates some of the drawbacks of hitting nulls, but I don't think it quite adds up to the power of proven non-null references.

1. Sample value is a valid value of the type. for example for array of strings it would be empty or some other string rather than null.
2. The original questions about explaining things to compiler. The sample value will allow to fill extra cells with values without disturbing compiler's type checker. Whether the sample value ever leaks to the user of resizable sequence type, it is subject of another theorem, but the compiler will not need a hole in the type system just for arrays.

The sample value must be a valid value for the type, yes, but it is also something the user needs to implement and provide an instance of for no other purpose than to satisfy the type system when implementing the vector, since the user will never see the sample value returned from the vector (unless they added it explicitly).

It's all very well to say it's just an "empty" value, but that's not particularly meaningful for every type. What's an empty mutex? What's an empty thread? What's an empty Factory pattern implementation - one that provides empty instances of other types?

My beef is that this is something that the user needs to implement for every type that they might want to put into a vector, but the design overhead of implementing it doesn't seem so trivial to me.

but the design overhead of implementing it doesn't seem so trivial to me.

I don't get what's so difficult about a generic nullable type:

type 'a option = None | Some of 'a

module Array = 
struct
  type 'a array
  
  (* initializer and array size provided *)
  val make_array: 'a -> int -> 'a array
  val at: 'a array -> int -> 'a
end

Why is this so hard to use?

You've applied his quote to the wrong context - he was writing here about why we shouldn't force users to come up with a "sample value" when they create a vector.

Right, but I'm asking why that's such an onerous requirement. "make_array None 1000" doesn't seem like such a burden.

His quote was about the difficulty of creating a sample value of arbitrary type.

Are you proposing that whenever it's difficult to create the sample value for a Vector[T], that Vector[Maybe[T]] be used instead? That seems clearly worse to me than the alternative design of hiding the Maybe type in the Vector implementation, but regardless, I think his point was reasonable.

From my reading, he was saying that null was a valid value in the circumstances in which no value had been set. That sounds like the option/Maybe type to me.

If a default value of the actual type is available, then use that. If you need a concept of "unset index", use option/Maybe. That's what it's there for.

From my reading, he was saying that null was a valid value in the circumstances in which no value had been set.

I don't see how you could get that from his post.

he was saying that null was a valid value in the circumstances in which no value had been set

I wasn't trying to say that. However, I don't want to labour the issue and I've already said my piece (or three).

Yep. Empty thread is a problem. Particularly from point of view of GC. BTW ML seems to use this pattern for mutable ref object.

Then the next trivial solution would be to keep account of bound elements in the mutable array primitive.

A simple way would be just to track amount of bound elements and to require that get should be from bound element range and set element should check that index is within bound or it increases bound by one. Array copy would be an another way to increase bound. This will cause +1 integer in the array object. And +1 read and +1 write operations for writing to unbound cell. This could be done in the array primitive, so compiler would not need to be explained anything special.

From what I see, non-contiguous ranges would require a bit mask possibly with more complex array access arithmetics.

You couldn't fill the array with a sample value if the value type imposes, for example, each instance to be referenced only once. So I don't think that is general enough.

Whether you use a sample value or Maybe, isn't there an irregularity here? If you request an index within the buffer capacity but outside the vector size, do you get a value in return? What if you request an index outside the buffer capacity?

Bounds checking looks like a better alternative as there is no irregularity.

I feel this array problem is poorly specified. It isn't as though arrays are being used as collections; instead, they're being used as blocks of memory resources to be managed in user space.

Perhaps we should figure out the real problem here before seeking a solution to it. I hear that solutions are often obvious when the problem is well specified.

I suspect the real problem depend on whether you're standing at a high level looking down (wanting collections that meet mutation and access/indexing and ordering and uniqueness and persistence constraints you specify), or sitting at a low level looking up (wanting efficient and safe access to memory resources such that programmers can build specialized collections to meet system needs).

Approach either of those problems and solutions for 'non-null mutable resizable vectors' become available... on the HLL side where compiler support for collections that are usefully indexed becomes 'baked in' to the language, and on the LLL side where one makes memory resources into first-class language commodities that may provably meet safety and security conditions.

"Memory resources into first language commodities" - the usual way this is done for data of arbitrary size is through arrays. And yes, I am interested in the low-level end of things, wherein the language is simple - i.e. few primitives - and collections etc. are built from them.

If I want to implement a vector type that is parameterized on its element type, it appears that I must require the user to implement the Null Object pattern for each and every single type that might be contained in the vector, and provide me with an instance of the same, simply to satisfy the typechecker.

Either that, or the underlying array-like primitive needs to support null references, and needs to use runtime checks to provide static safety.

Arrays do not provide first-class access to memory resources. They impose a particular 'view' on memory resources. It is in aiming to meet this view that you run into the problem you've been harping - in particular, because 'arrays' are 'collections' and each entry in a collection must have a valid type.

Of course they're not raw-metal ways to access memory resources. If one was dealing with raw-metal memory, you would have far worse problems than null references.

I'm sorry if it seemed like I was harping on, but it just seemed to me that there was an elephant in the room that nobody was pointing out, with too many people seemingly content to implicitly and smugly disclaim all those very successful languages that do have null references, when the only practical approach seems to be post-hoc static verification with the aid of annotations.

It is my impression that the problem you've been describing has an existence only insofar as your failure to consider mechanisms to manage memory resources other than use of arrays.

And I did not suggest raw metal memory access.

Language support for memory resources is still free to abstract that access (e.g. to allow for persisted memory resources, expandable memory resources, memory resources that are largely in a file, automatic compression or encryption, track annotated cleanup properties for private data, etc.), to support representation management (varying layouts and encodings for 'values' even of a given type), to recognize hierarchical management (so a subprocess can acquire resources then dole them out to sub-sub-processes), and perform verifications (the basic ones being that a subset of memory is initialized to a valid encoding before being 'viewed' as a particular type, and that memory is consistently 'viewed' as a particular type prior to being released) impose safety and capability security limitations on use (e.g. guaranteeing access rights to a memory resource cannot be forged), etc. for any given memory resource.

But, at bare minimum, as a sort of unchecked capability, the LLL would offer ability to determine proper alignment and size, request blocks of memory of a given size and alignment, and do so separately from initializing the memory in preparation for a particular view (i.e. use of 'new(address) object(constructor-args);' in C++).

Thank you for pointing out my failures. I would appreciate references etc. outlining approaches to handling memory resources so flexibly in a provably type-safe and memory-safe way.

The list above is to make it clear that 'first-class support' and 'bare metal' are completely different concepts. I suspect one would need to sacrifice direct access to support object capability based, versioned pointers, transactional memory, memory-mapped persistent resources, etc.

Making memory resources independent of type is as simple as adding (to EVERY constructor that potentially requires memory) a source from which it is to allocate its memory. Safety is achieved pretty readily if allocation is a once-only event. With C++, the 'placement new' provides a less than perfectly safe form of this... in that it allows multiple 'new(address)' calls on the same address.

Of course, there's currently no such thing as a strongly typesafe language with explicit memory deallocation... Deallocation safety might be doable if one can prove that all 'views' of a particular memory resource will occur 'through' a particular object (i.e. one promising approach is use of object capability to prove safety of certain deallocations; systems like Emily that statically study leak of capability already exist), but perhaps should be left to garbage collectors or suggested then left to compile-time inference.

The above paragraphs offer some keywords for you to look up in the study. I've not read any papers on the subject since my own interests lie more in the direction of the high-level-language approach to mutable collections; my interest in management of memory resources has more been towards achieving safe and efficient hardware I/O.

Anyhow, your goal is to support vector<T>, and you want the vector to be growable to some level, and you do not want to deal with a full 'array' by ensuring every entry is initialized to some 'default value' ahead of time. In this case, you would ask the system for a block of memory (the memory is currently untyped), to which it would respond with a block allocator. You would then need to use the block allocator when constructing new values from the block of memory. The values constructed would be subject to the regular sorts of typechecking. The typechecker would need some extra intelligence (likely in terms of dependent typing) to guarantee such invariants as 'safely allocated values are accessible in this block for offsets less than the 'size' value'.

Allocation failures would likely be checked dynamically, just as they are in most languages today, but some patterns of allocation might also be statically checkable with invariants. (Not that type safety is required to be static.)

This approach would achieve the critical invariant for memory safety, which is that an area in memory is either unallocated or is viewed the same way in all parts of the program.

In terms of flexible features stated in my above statement, note that they'd be applied to the allocator (which might be from a persistent store, or be told to upon deallocation wipe the area of secret data so it can't be retrieved, or might be expandable). These features for first-class memory resources must be applied to representations of memory resources, not regular values or objects.

You haven't told me anything I don't already know re placement new or explicit deallocation.

I was specifically interested in how you suggested that these constraints be handled simultaneously:

* Type safety and memory safety
* Supporting only non-null references
* Building a resizable vector abstraction out of more primitive parts (i.e. not baking a resizable vector / dictionary / whatever into the language)

by using "mechanisms to manage memory resources other than use of arrays".

What you do seem to have suggested in the second half of your reply, as near as I can make out, is some kind of abstraction called a "block allocator" which can be indexed in a type-safe way, because the type system knows about its total size and its current allocation size. That also seems to imply that it is parameterized by the type it indexes to (otherwise how does the type system know that the user hasn't done a switcheroo?).

Thus, it seems to add up to a kind of resizable, but only up to an allocation-time limit, mutable vector primitive; a lot like an array with strings attached.

That also seems to imply that it is parameterized by the type it indexes to (otherwise how does the type system know that the user hasn't done a switcheroo?).

The allocator would not be parameterized by type. The vector would be. The type system would need to prove that all indexes into the vector, at least up to some dependent value, are of the same type, which would involve proving that the allocator isn't being used by any other object.

If you wish to avoid dependent typing, then yes, the allocator would need to be parameterized by type if one is to allow simple automated theorem provers to prove the space used by the 'vector' isn't also used for other purposes and types.

Thus, it seems to add up to a kind of resizable, but only up to an allocation-time limit, mutable vector primitive; a lot like an array with strings attached.

The block allocator, which would only be one type of allocator (not primitive), was aimed to provide 'direct' access to memory. If you're aiming to forgo that limit, and you're willing to take a hit in terms of indirection, it would not be difficult to have the block allocator providing data out of what is essentially a unique address space (e.g. a file, which may be volatile or persistent). Admittedly, if you do it this way then pointers into the vector cannot be expressed simply as pointers into memory, since they would also need to carry information about their address space.

The allocator approach to memory management allows such 'features' to be attached to the memory resource transparently to the type system (at least so long as 'representation' and memory layout aren't themselves embedded into the type system). That is a big win.

And other than the need for a theorem prover that can analyze object capability (who might be using an allocator) and the extra syntactic burden of associating allocators with constructors and representations with values, there are no strings attached to this approach that aren't already a problem with arrays. Arrays have their own strings attached... e.g. the need to 'initialize' each entry in the array to a valid initial value.

All that said, I honestly don't care for mutable non-persistent arrays... all my work is towards transactions, versioning, etc. I'd probably implement a 'mutable vector object' as an actor that updates and replies to messages requesting updates by creating variations on immutable collection values.

You've already mentioned another practical approach, namely building such arrays into the language.

The array of Maybe solution is also valid and is actually a special case of the default value solution and need add no overhead at all.

Haskell inadvertently solves this problem without null references as well. For unboxed arrays, null references wouldn't work because the objects aren't pointers and so some variation of the "default value" approach is needed. For boxed (mutable) arrays in Haskell, uninitialized cells can be filled with 'undefined'. undefined is semantically equivalent to an infinite loop, in practice an error construct is used to give a friendlier message. In this context, accessing these elements would be no different in quality than an array out of bounds exception (you could, in fact, partially handle out of bounds exceptions by stick the appropriate error thunks into the uninitialized values.)

So here are three approaches, none of which require any kind of analysis.

I doubt any current language today has null references simply because the designers couldn't think of a way to handle uninitialized storage.

That will work for reference types, but what about unboxed value types, like int32. It maybe not quite a haskell problem though...

The maybe approach still works for this in BitC, but it doesn't address part of the objection, which is that requiring an option of any sort in order to support expansion is problematic.

The implication above that the array/vector itself could check where it is initialized just as it checks for bounds errors is possible for both unboxed and boxed types. In typical idioms the check can be removed at compile time with dependent typing tricks and a not very powerful solver.

But the part of this that has me stumped is the assumption that resizable arrays are important. Offhand, I can't think of a language that implements them. In those that simulate this (e.g. Python), the "array" is actually a "map", and the problem that the author is concerned about does not arise. Unbound map locations either raise an exception on access or explicitly return "not found" in some fashion.

The case that seems to me to exist in many languages — and the case that continues to concern us in BitC — is the problem of initializing a non-resizable array of immutable cell type. The immutability means that you cannot defer the initialization to assignment time by supplying a dummy value. Our solution, which is decidedly inelegant, is to allow the user to pass in a function that produces the desired initializers for each position. We also have the usual panoply of list->vector and such like operations in our library.

the part of this that has me stumped is the assumption that resizable arrays are important

If it was me that you were stumped by, let me clarify: some kind of resizable vector abstraction is very useful and exists in almost all imperative languages; but it doesn't need to be a primitive, it's even preferable that it isn't a primitive (particularly one that replaced arrays), when considering the need to reduce the number of abstraction layers in user-defined data structures.

It was in the implementation details of this very useful abstraction, that I was interested, when taking - for purposes of argument - a hard line on non-null.

Re initializing arrays of immutable values, it seems to me that is a general limitation of the functional approach, and is usually tackled using logarithmic-performance structures instead.

Okay. That makes sense now. Thanks.

it's even preferable that it isn't a primitive (particularly one that replaced arrays), when considering the need to reduce the number of abstraction layers in user-defined data structures.

I'm curious about this assumption. In what way do you see a "need to reduce the number of abstraction layers in user-defined data structures"?

Do you see the problem to be abstraction layers rather than implementation layers?

I have a fair amount of skepticism, bordering on cynicism, about the existence of "sufficiently smart compilers" - particularly compilers that themselves need to be very fast.

There is also the degree of control the user expects over low-level details. When composed abstractions start conflating, perhaps based on optimization levels, the user may be surprised, even if the result is efficient. If it's a type-unsafe language, then the user may even have made assumptions about the implementation details that the program relies on for correctness.

For these reasons, layers in abstraction tend to be synonymous with layers in the implementation, when considering the practical aspects of implementing a commercial compiler (Delphi in my case).

I have a fair amount of skepticism, bordering on cynicism, about the existence of "sufficiently smart compilers" - particularly compilers that themselves need to be very fast.

Me too. I don't want sufficiently smart compilers. I want dumb compilers that can follow suggestions for implementation strategy from sufficiently smart programmers and from expert systems with good memories. And I want an IDE capable of representing search spaces such that a programmer can help guide compilation. Expert systems or databases could remember, on a per-project granularity, what worked before... and thus massively speed it up when compiled later, potentially gaining time to consider new optimizations in each edit-compile-test cycle. This compilation data could be exported for compilation on other machines, perhaps even combined with other data.

There is also the degree of control the user expects over low-level details. When composed abstractions start conflating, perhaps based on optimization levels, the user may be surprised, even if the result is efficient.

Achieving performance guarantees (e.g. realtime & fixed footprint) is also relevant, and it is difficult for a compiler to achieve goals for a subsystem-as-a-whole if myopic programmers are given great control over intermediate details of representation, especially if said users wish to reuse code and libraries written with the same level of myopic control.

If it's a type-unsafe language, then the user may even have made assumptions about the implementation details that the program relies on for correctness.

Yes, that is a real problem... not just for type-unsafe languages, either. E.g. even in a type-safe actors language, for which message arrival order is indeterminate, the user might make assumptions about message arrival orders for messages from the local machine.

Similarly, if 'set' is defined as 'unordered', but the default implementation is sorted order rather than hash, programmers may depend on this ordering... thus making their code unportable and less optimizable.

Perhaps a debug compiler should shake a user of these assumptions by design. Compiler writers would identify places where programmers are depending on particular implementation details, and code in deterrents (e.g. pseudorandom message ordering, or occasional 'dropped' messages when simulating unreliable connections) to help ensure that writers aren't essentially unit-testing implementation details for the language. When it turns out a feature is needed, such as control over message arrival orders and scheduling on a local machine, then that can be encapsulated in a language concept (like a 'kell') to which programmers can attach schedulers and message queues for actor configurations.

This isn't so much of a problem, Haskell works very well in this case.

You just have to change your habits : instead of creating an array and then populating it, both process are simultaneous. The usual objection to that is that often you have to use values already in the array to initialize another index but in Haskell, with the lazy evaluation, you perfectly can refer to an array you're creating in it's own initialization.

Another case is that several pass are made on the array to initialize it and foregoing this process would complicate the task. Haskell introduce accumulating array for that and it cover most usage I have seen. Of course for performance reason this initialization process is imperative internally but it is completely pure from the outside.

Maybe == null for reference types (for mutable types, where it makes a difference). Building the vectors in, I'm less enthusiastic about.

I'm not very familiar with the Haskell undefined construct you describe, but they sounds somewhat like how null values already act in other languages, only with more drastic consequences.

Lazy construction?

I think that the answer to your question is that you still need nullable type, just that it's the wrong default to have.

There's no 'magic way' to eliminate null reference errors but reducing the number of possibility of these error is already a big step.

He basically punts on the array issue: one example he suggests is requiring that a closure be passed to a library routine which builds the array on demand and calls back for each element; another is using the existing List or Vector classes; and another one is array comprehensions.

None seem very suitable for implementing a vector from scratch.

From what I could briefly make out, Dylan solves my mutable vector implementation problem (see above) with built-in collection classes. If I'm wrong, feel free to correct me!

The element-accessor signals an exception if the index is not in the bounds of the collection. And yes, they're built-in.

Or was the mistake making all references nullable, rather than just those that are declared as such?

There are two mistakes. One mistake is providing a 'sum' type (eqv. to Just Object | Nothing) without recognition of the typechecker. The other mistake is joining this sum type at the hip with the idea of references, such that you cannot have one without the other.

These mistakes may, and I suspect should, be resolved independently. Thinking there's just one mistake, and thus just one language feature to solve it, might very well be a third mistake.

In an OO language, one uses the NullObject pattern. In my experience this often has strong advantages over using null references.

This issue is one of several reasons that BitC requires initializers to be pure. Technically, a BitC initializer can source but cannot sink a mutable location. The effect is that the mutability of global locations does not take effect until the start of main(). In our case this was motivated by ensuring a well-defined initialization order, but our solution closed this hole at the same time.

I do think that from the perspective of concurrent GC it is probably a good idea for references to be nullable at the GC level of abstraction even if such references are disallowed at the program's level of abstraction. I don't think that this introduces any of the issues that Tony mentions.

It's also impossible to have mutually recursive data structures without providing for object escape or a nullable type.

Or a recursive data binding construct (datarec?) or mutable locations.