RFC: `Object` and `ObjectArray` types

Stream: batteries

[François G. Dorais]

I'm cleaning up some old stuff and I found something that I occasionally find useful and might be better off in Batteries.

The Object type is a wrapper for a value of any type. It's handy to store values of heterogenous type.

Here is a simplistic example:

structure NatOrString where
  isNat : Bool
  val : Object
  type_eq : if isNat then val.type = Nat else val.type = String

Of course, Sum Nat String works just fine for this type, but you get the idea...

A better use case is ObjectArray which implements arrays with items of different types. The type information is stored in a function, which gives more flexibility how to actually store the type info (e.g. an array, a list, a fixed pattern, etc.). As a result, a limited set of functions are implemented. For example, append needs slightly different implementation depending on how the type info is actually implemented since that leads to different ways of appending the type info.

Here is some sample code using ObjectArray:

def foo : ObjectArray 3 fun | 0 => String | 1 => Nat | 2 => Float :=
  .mk fun | 0 => "foo" | 1 => 42 | 2 => 3.1415

Full code is at batteries#812

[Joachim Breitner]

There were previous discussions about such dependent arrays (often called DArray). Would be great to have them! For example for flattened associative arrays, packing keys and values directly in a single array.

In your code the universe parameters are implicit, but I assume that your DArray does incur a universe bump, because Object does?

[François G. Dorais]

Yes, there is universe a bump because the implementation uses Object. Annoying but hard to fix.

[François G. Dorais]

The only way I know how to fix the universe bump issue is to fiddle with lean internals. That wouldn't fit well in Batteries but I could be done in core.

[François G. Dorais]

There's a lot of discussion around DArray. Too much to summarize here. In any case, ObjectArray is not the ideal implementation for DArray.

[Max Nowak 🐉]

If you can provide a list of types as a parameter to Object, you can use them without a version bump

[Max Nowak 🐉]

Universe bump*

[Max Nowak 🐉]

So have a list of all possible types that may occur inside the array, and pass that as a parameter everywhere. And then instead of storing Type, you store the index into that array

[Mario Carneiro]

Is this docs#Dynamic ?

[François G. Dorais]

It's not the same as Dynamic since there is no name for type i.

However, I implemented a Union type and used it to make @Max Nowak 🐉's idea work. This is now in batteries#813.

DArray without the universe bump is accomplished!

[Mario Carneiro]

Isn't Union just Sigma?

[François G. Dorais]

Yes, I just realized that! :man_facepalming: Long day... I'll fix that tomorrow today.

[Mario Carneiro]

I think it's also not as good (runtime-wise) as my original unsafe-happy implementation of DArray because it has an additional indirection in each element of the array, since each cell now needs to store its index

[Max Nowak 🐉]

Yeah I think the suggestion I gave is not a good idea. It was merely a way to circumvent the universe bump.

[François G. Dorais]

Yes. My hacked C-implementation also doesn't need to store indices like that. But this will work for now until core implements the right way.

[François G. Dorais]

I figured out a way to avoid storing indices without actually going down to C... It's terrifyingly unsafe though!

[Max Nowak 🐉]

The approach with Object doesn’t seem so bad to me. All you need is knowledge of which index has which type. If I have “forall i, arr[i].type = String” for example I would know the shape of each cell. This knowledge can be in Prop. This wouldn’t need unsafe either. But I’m not a maintainer and have barely dedicated any thought to this, so maybe ignore me.

[Max Nowak 🐉]

Actually I don’t know any of the design goals behind this, so definitely ignore me.

[Mario Carneiro]

The major drawback of the Object type is the universe bump. This makes it unusable in lots of places we would like to have it

[François G. Dorais]

The current batteries#813 avoids the universe bump and avoids actually storing indices. The latter part needs some stress testing but it seems to work fine so far...

[François G. Dorais]

Actually, since the type definition of DArray is now just a model for the kernel to digest, it might be even easier to define it as:

structure DArray (n : Nat) (α : Fin n → Type _) where
  get (i : Fin n) : α i

The actual implementation would still work as it does now, but the proofs would be even easier, I think.

[François G. Dorais]

That doesn't seem to work... I think it's because overriding DArray.get doesn't actually override the structure projection.

[François G. Dorais]

Yeah, that's it. It works fine if I use an inductive instead:

[François G. Dorais]

inductive DArray (n) (α : Fin n → Type _) where
| mk (get : (i : Fin n) → α i)

[James Gallicchio]

François G. Dorais said:

That doesn't seem to work... I think it's because overriding DArray.get doesn't actually override the structure projection.

is this a known bug/feature..? maybe another place the compiler should emit a warning

[François G. Dorais]

batteries#813 looks pretty nice now but it's not ready yet. The recursors need to be reimplemented for match to work... That could take a while. Anyone know the minimal set of recursors that need to be redone?

[Mario Carneiro]

James Gallicchio said:

François G. Dorais said:

That doesn't seem to work... I think it's because overriding DArray.get doesn't actually override the structure projection.

is this a known bug/feature..? maybe another place the compiler should emit a warning

lean4#2292

[Mario Carneiro]

ping @Leonardo de Moura , that PR is an easy fix to a year old bug in the old compiler which you self-assigned a while ago, and it's blocking "extern type" style APIs like DArray here

[François G. Dorais]

It looks like recOn and casesOn are enough to make match work properly. It's time for some more serious testing...

[François G. Dorais]

After a bit of rest, I cleaned up batteries#813 and it is now ready for community review.

[François G. Dorais]

I found @Mario Carneiro's earlier work (I don't know why I didn't look for that sooner!) and I started stealing some useful stuff :pirate_flag:

I want to keep this PR from blowing up, so I'll leave a lot for follow-up work. For example, foldl, foldr and forIn are almost surely better left to the near future than this PR.

I reluctantly added push and pop. Having the types specified by a function makes these (and append) a dependent type purgatory. I think these are better off in follow-up work where the type specification has a specific representation.

[François G. Dorais]

The follow-up PR batteries#815 now has foldlM, foldrM, map and even a ForIn instance so that for ... do can be used to loop over dependent arrays.