Alternative List Definition?

Stream: general

[Mac]

So an alternative definition of a list is the following:

structure GetList (α) where
  len : Nat
  get : Fin len → α

I'm curious as to what this definition of a list is called and why it isn't used more in functional programming / type theory.

[Kyle Miller]

In Lean 3, that happens to be called docs#buffer, which I understand has special support in the VM to use more efficient data structures.

You likely see it less because the linked list definition tends to make for nice recursive definitions, and also it requires a dependent type system to use.

[Mario Carneiro]

In lean 4, it's called Array

[Mac]

Mario Carneiro said:

In lean 4, it's called Array

What do you mean by that? A Lean 4 Array is just a wrapper around List that has a special handling in the code generator -- it is nothing like this?

[Mario Carneiro]

Oh, did it change to List in the model? In lean 3 it was a Fin n -> A function. Both are lies of course

[Kyle Miller]

I think another reason this alternative list definition tends not to be seen (without special support like in Lean 3) is that runtimes tend not to memoize functions, meaning most times when you compute l.get i it would evaluate the Fin len → α function again. The usual inductive definition of a list gives the runtime places to store evaluated elements of the list.

The famously lazy Haskell runtime, for example, uses 0-argument lambdas ("thunks") to represent unevaluated expressions, and once a computation forces a thunk to evaluate to weak head normal form, the thunk is mutated in-place with the evaluated result. Constructors for inductive types, then, are a natural place to hold onto a number of thunks that you know will only ever be evaluated once. There is a trick in Haskell to memoize functions whose domain is the natural numbers -- and that's to replace the function with one that accesses the corresponding element of a lazily constructed list!

For what it's worth, while the underlying definition of Array is different, the library defines Array.size and Array.get, which correspond exactly to your GetList.len and GetList.get. It's missing a GetList-like constructor, but it's easy enough to define one (though I'm not sure what I wrote is idiomatic):

def Array.create (f : Fin n → α) : Array α := do
  let mut a := Array.empty
  for i in [:n] do
    if h : i < n then
      a := a.push (f ⟨i, h⟩)
  a

Once you have all these functions (along with some supporting lemmas) then there's not really a difference between Array and GetList other than computational efficiency.

[Mario Carneiro]

For your last definition, although it looks nice it bothers me a bit that there is a superfluous if-check. We can eliminate it like so (while retaining the tail recursive quality of the loop):

partial def Array.create (f : Fin n → α) : Array α :=
  go Array.empty 0
where
  go (a : Array α) (i : Nat) : Array α :=
  if h : i < n then
    go (a.push (f ⟨i, h⟩)) (i+1)
  else
    a

Unfortunately we had to go partial to make this work, and to show termination we need to add more stuff that might break the performance again, so at this point I would just use an implementedBy to define your function as the model and my function as the implementation

[Mac]

Kyle Miller said:

Once you have all these functions (along with some supporting lemmas) then there's not really a difference between Array and GetList other than computational efficiency.

It is certainly true that they are functionally equivalent definitions. However, it is the computational efficiency part hat interests me. I would think this model of a list would be much easier to implement computationally. A normal functional List essentially models a linked list data structure. However, a GetList models l a random access array. The get function would simply need to be an memory access (i.e., literally just a load instruction) from a given offset (which could, for example be part of the function's closure). That is why I was curious why a model like this isn't used more often.

[Mac]

In fact, to directly represent a memory slice, we could model a list like so:

structure Slice (α) where
  head : Nat
  tail : Nat
  get : (n : Nat) → (h : head ≤ n ∧ n ≤ tail) → α

I would think that such types would be much better models for computational reasons. (This one is unfortunately less pretty as there is no builtin Nat interval type as far as I know).

[Mac]

Admittedly, a Slice would be less useful in a pure contexts because the actual head and tail are real world artifacts, but the GetList abstraction resolves this by removing those details.

[Mario Carneiro]

It is certainly true that they are functionally equivalent definitions. However, it is the computational efficiency part hat interests me.

Like I said, both definitions are lies. The computational efficiency of array operations is determined by the implementation of the functions, and means that Array.get is O(1) (assuming O(1) memory access), even though if you take the model seriously it looks like an O(n) definition to walk the List. But the List doesn't actually exist unless you call the function Array.mk, which despite having the appearance of a "mere wrapper" is actually a computationally heavy conversion function. Same for Array.data, which is not O(1) even though it looks like a field projection.

[Mario Carneiro]

A normal functional List essentially models a linked list data structure. However, a GetList models l a random access array. The get function would simply need to be an memory access (i.e., literally just a load instruction) from a given offset (which could, for example be part of the function's closure). That is why I was curious why a model like this isn't used more often.

If we assume no special runtime support for arrays and just consider a generic runtime using closures and linked lists, then a function Fin n -> A is stored as a closure, and the performance cost of calling this function depends on the function that was stored. In theory it can be as good as O(1), for example if the user stored a constant function in the "array", but assuming that you actually want to store n different elements with no special rule for generation, for example if you are buffering characters from an input stream, then a pure functional data structure cannot do better than O(log(n)) access time, but clearly there are linear size data structures that achieve this bound (just use a balanced binary tree), and if you wrap the accessor for such a data structure in a closure then you can get this performance in a Fin n -> A array as well.

[Mario Carneiro]

Here's a less lying way to present the interface of Array:

constant Array (α : Type u) : Type u := sorry

@[extern "lean_array_mk"]
constant Array.mk : List α → Array α := sorry

@[extern "lean_array_data"]
constant Array.data : Array α → List α := sorry

However this is a lot less convenient because you don't get things like a.mk.data = a := rfl like with the structure definition, and also you can't really fill those sorry's as written because constants can't depend on each other like this, you have to stick the whole spec in a structure and make one constant over the whole thing (this is how Float is defined, for example).

[Kyle Miller]

An interesting design for providing a data structure with O(1) access is in Dex, which has a special function arrow a => b when a is a finite type, and it stores the function as an array. (Though these aren't functions precisely.)

[Mario Carneiro]

@Mac I don't really think of a closure as a data structure. What it actually provides is the way to abstract over data structures through dynamic dispatch, but you still have to have an implementation behind the indirection and that implementation ultimately has to consult some actual data structure which determines the computational efficiency of the result. (That's not strictly true; a closure's actual data content is approximately the same as an inductive type, that is, a discriminant (the function pointer) and a tuple of local variables, so you can certainly use recursive closures to build real data structures, but this usually ends up being a less efficient version of inductive so I don't recommend it.)

[Mac]

Mario Carneiro said:

Mac I don't really think of a closure as a data structure.

I have always thought a closure as simple data structure which is a function (pointer) together with its environment (i.e. a struct of related data the functon references).

[Mac]

Mario Carneiro said:

If we assume no special runtime support for arrays and just consider a generic runtime using closures and linked lists.

I am confused about what you are assuming here. Why would a generic runtime with just closures and linked lists be a reasonable default assumption? Are there some constraints you are assuming about the representations of functional data structures that I don't understand?

For example, is there some reason the an array like [2,8] could not (in some theoretical functional language) just be translated to {len := 2, get := fun | 0 => 2 | 1 => 8} : GetList and the get function thus translate to an array access to an allocated [2,8] real array in its closure?

[Kyle Miller]

@Mac I think the point is that with GetList you need to signal to the compiler that you want the function to store its values (the extension of the function), rather than the usual, which is to store a closure (the intension of the function). If you extend the language to give you the ability to mark when a function's extension should be stored (which certainly should not be the default!) then I don't see why it can't be translated in the way you suggest.

But also, if you're going through the effort to make a language extension for this, which might only ever be useful for implementing arrays, one wonders if it would be better to do what Lean 4 does, which is to create a general interface to allow theoretical definitions to be replaced by efficient code.

[Eric Wieser]

I don't know if you're aware of this already @Mac, but we have ![2, 8] in mathlib that builds essentially that function

[Mario Carneiro]

For example, is there some reason the an array like [2,8] could not (in some theoretical functional language) just be translated to {len := 2, get := fun | 0 => 2 | 1 => 8} : GetList and the get function thus translate to an array access to an allocated [2,8] real array in its closure?

This just shifts the question to how arbitrary-fanout matches are implemented. If, like lean, this is represented as a nested if-else expression (especially since it's probably of the form "if zero then this, else call this nested function of a similar form") it's no better than a linked list.

[Mario Carneiro]

I am confused about what you are assuming here. Why would a generic runtime with just closures and linked lists be a reasonable default assumption? Are there some constraints you are assuming about the representations of functional data structures that I don't understand?

I didn't mean that to be an exhaustive list. In particular I am also assuming that the runtime supports general inductive types (of fixed arity), i.e. pairs and sums, which is enough to build most lisp style functional data structures. This is the setting where you normally get the log(n) lower bound, because the core data constructor has finite branching factor so representing an object of size n requires log(n) constructor depth. Using functions with if-statements don't get you out of this, because if statements also have finite branching factor.

Arrays are a fundamentally different thing in this setup, because they have arbitrary fanout. (Technically, it's still log(n) since you have to read the index which has size log(n), but we usually ignore that in the RAM model.) Large matches compiled to jump tables seem to be similar to arrays in this sense, but I think they still have finite branching factor if we assume all such matches are compiled up-front and there is no dynamic code generation. In any case we generally don't want to generate code proportional to the size of the array, that would be very wasteful.

[Mac]

Mario Carneiro said:

This just shifts the question to how arbitrary-fanout matches are implemented. If, like lean, this is represented as a nested if-else expression (especially since it's probably of the form "if zero then this, else call this nested function of a similar form") it's no better than a linked list.

I didn't realize that large fanout was implemented as successive if-else trees. From my understanding, the general best practice for such things (which would parallel a switch in C/C++) is to compile them down into an constant array access (if the indices are reasonably adjacent) or a special no-collision hash map (if they are not). If a result is more complex than a single value, this might be a map to function pointers / labels. In fact, LLVM, for example, even has specific IR instruction (the switch) for implementing the later. Which, as the docs say, is usually implemented through such a lookup table (except in some targets that don't support it).

[Mac]

Kyle Miller said:

But also, if you're going through the effort to make a language extension for this, which might only ever be useful for implementing arrays, one wonders if it would be better to do what Lean 4 does, which is to create a general interface to allow theoretical definitions to be replaced by efficient code.

Well there are two problems with the Lean-like implementation (though these might be improved in Lean in the future). Either the implementation is is also written in Lean, which doesn't solve the representation problem, or it is implemented in an external language, which means the definition In Lean is lies and can't be analyzed within the functional language. The point of the model / implementation combination I am discussing is that, with it, you can get a one-to-one model to implementation correspondence. The fanout get is a proper truthful abstraction of an array access that can also be directly implemented as such.

[Mac]

Eric Wieser said:

I don't know if you're aware of this already Mac, but we have ![2, 8] in mathlib that builds essentially that function

Cool, that's neat! My question is more though why this is not the general functional paradigm for lists.

[Mario Carneiro]

Mac said:

From my understanding, the general best practice for such things (which would parallel a switch in C/C++) is to compile them down into an constant array access (if the indices are reasonably adjacent) or a special no-collision hash map (if they are not). If a result is more complex than a single value, this might be a map to function pointers / labels. In fact, LLVM, for example, even has specific IR instruction (the switch) for implementing the later. Which, as the docs say, is usually implemented through such a lookup table (except in some targets that don't support it).

This is assuming that the data is known up front so that the compiler can take a stab at optimizing it. Normally, if you have a piece of code manipulating arrays, the code itself is quite small even if it manipulates huge arrays. So there is no giant switch for the compiler to chew on. The only time this comes up is when you are using the code to store a large static array in the binary, it doesn't handle arrays coming from the runtime environment.

[Mac]

Mario Carneiro said:

The only time this comes up is when you are using the code to store a large static array in the binary, it doesn't handle arrays coming from the runtime environment.

I think the runtime case is actually easier. There you could have something like constant alloca (α : Type) (size : USize) : IO (Fin size.toNat → α). that allocates the runtime array and returns a wrapped lambda which performs the array access.

[Mac]

For cases where the runtime array is coming directly from the real world (like the argument list to main), even less lying has to be done as those objects are already opaque. The functional runtime can freely fill in get with an appropriate lambda accessing the proper place in memory (such as the beginning of the executable stack for main arguments).

[Mario Carneiro]

Mac said:

Mario Carneiro said:

The only time this comes up is when you are using the code to store a large static array in the binary, it doesn't handle arrays coming from the runtime environment.

I think the runtime case is actually easier. There you could have something like constant alloca (α : Type) (size : USize) : IO (Fin size.toNat → α). that allocates the runtime array and returns a wrapped lambda which performs the array access.

That function has to be implemented somehow though. If you just say "it's abstract and implemented by magic" then it's no different from lean's Array.get, except that lean doesn't wrap the result in IO because array creation can be a pure operation.

[Mario Carneiro]

Lean actually has a much better thing since it also supports destructive set, not just get. That function representation can only support read-only arrays

[Mac]

Mario Carneiro said:

That function has to be implemented somehow though. If you just say "it's abstract and implemented by magic" then it's no different from lean's Array.get, except that lean doesn't wrap the result in IO because array creation can be a pure operation.

A rough example implementation:

abbrev Addr := USize

@[extern c inline "(sizeof(size_t))"]
constant Addr.byteSize : USize

@[extern c inline "((size_t)(malloc(#1)))"]
constant malloc (size : USize) : IO Addr

@[extern c inline "(*((lean_object**)(#1)))"]
unsafe axiom load {α  : Type} (addr : USize) : α

unsafe def unsafeAlloc
(α : Type) (size : USize)
: IO (Fin size.toNat → α) :=  do
  let addr ← malloc (Addr.byteSize * size)
  return fun i => load (addr + i.val.toUSize)

@[implementedBy unsafeAlloc]
constant alloc (α : Type) (size : USize) : IO (Fin size.toNat → α)

Admittedly, the alloca isn't very useful as you can't actually fill the array with values. But the point of this proof of concept was just to show how this model corresponds closely to the bare metal implementation and thus lies a lot less. I can provide a more feature complete model if you really want one though.

[Mac]

Mario Carneiro said:

lean doesn't wrap the result in IO because array creation can be a pure operation.

I mean to, a certain extent, any operation can or cannot be pure based on what one wishes to consider as relevant state. Even basic mathematical operations (like addition) still change things like register state. Thus, if one wants to include that in their I/O model then a function like add would be impure and need to occur in an IO monad. Purity, to me, has about whether conceptually the operation is to occur in the 'real world' or happen in abstraction land.

Thus, to me, allocating an array, and more generally, the stand concept of an array, is an impure concept because arrays are defined as being allocated consecutively in memory, which is a requirement on their 'real world' representation. Something like GetList would be the pure analog (of a read-only array) because it has the same abstract functional structure (i.e., random access lookup), but says nothing about its implementation. A List, on the other hand, does not have the same structure (it models iterative lookup) and thus a does not strike me as a good model. You can still model an Array as a List but then you are lying about its structure and the operations you are performing, and I personally don't like that approach.

[Mario Carneiro]

I mean to, a certain extent, any operation can or cannot be pure based on what one wishes to consider as relevant state. Even basic mathematical operations (like addition) still change things like register state. Thus, if one wants to include that in their I/O model then a function like add would be impure and need to occur in an IO monad.

Well, yes. But reading that the other way around, saying that a given operation is pure is indirectly putting constraints on the observable states of the machine, and making certain properties of the runtime inaccessible. Register states are certainly among the things on the FP cutting room floor.

Thus, to me, allocating an array, and more generally, the stand concept of an array, is an impure concept because arrays are defined as being allocated consecutively in memory, which is a requirement on their 'real world' representation.

This is only if pointer values are accessible, and FP languages almost universally deny access to this information. Without pointer values, "consecutively in memory" is not a concept that can even be stated. Runtime behavior is a little closer to the mark (i.e. the characteristic property of an array is the way in which its performance characteristics differ from a linked list or tree), but the time taken to execute an operation is another verboten property.

You can still model an Array as a List but then you are lying about its structure and the operations you are performing, and I personally don't like that approach.

An array is like a list in that it stores a sequence of values. All the provable properties about arrays and lists are the same. Lists are preferable to functions because it is easier to prove theorems about lists by induction than work with fin functions (just take a look at the relative sizes of the two theories in mathlib for an idea).

[Mac]

Mario Carneiro said:

This is only if pointer values are accessible, and FP languages almost universally deny access to this information. Without pointer values, "consecutively in memory" is not a concept that can even be stated. Runtime behavior is a little closer to the mark (i.e. the characteristic property of an array is the way in which its performance characteristics differ from a linked list or tree), but the time taken to execute an operation is another verboten property.

I think this gets to the heart of the matter. I guess the model desired depends heavily on what kind of things you are hoping to do and prove things about. As a computer scientist and a security researcher, runtime complexity, the location of objects in memory, register state (even undocumented hardware architectural state) are interesting proof points for me (for example, to reason about things like Spectre and Meltdown). In math, of course, most of this stuff does not matter, but it does heavily in systems, compilers, and security, which is my general domain. As such, I definitely don't want those things on the cutting room floor. :P

What's neat about Lean is that it is perfectly capable of operating and reasoning at this level. For example, Joe Hendrix and the team at Galois Inc use Lean for analyzing such systems. Admittedly, other high performance functional languages (such as Haskell) can do low-level computation as well and I know Coq is used to verify some formal hardware systems. Lean, however, appears to be somewhat unique in that it can do both in the same language. At the same time, it can do high level theoretical math. In fact, I am constantly impressed at just how good of a truly general, general purpose language Lean is.