Fin basics

Stream: std4

[Mario Carneiro]

Is there a PR about this somewhere? I could have sworn there was something that upstreamed Fin.cons et al and now I need it and can't find it

[James Gallicchio]

Not that I know of... what do you need it for now?

[Mario Carneiro]

I started writing DArray :)

[James Gallicchio]

did my scuffed implementation inspire you to rebuild a reasonable version? :joy:

[Mario Carneiro]

the basics aren't too hard, it's blocked on lean4#2292, so I'm just going through and copying the Array interface and push will need some fin stuff

[James Gallicchio]

I'm somewhat unconvinced that anybody actually wants push on a DArray, but I can help upstream the fin vector file if you'd like

[Mario Carneiro]

well you have to get elements in there somehow

[Mario Carneiro]

using ofFn is only suitable for static arrays

[James Gallicchio]

"can we have push"
"we have push at home"
the push at home: .ofFn

[James Gallicchio]

Yeah. Did you have an application of DArrays where the size changes? Iirc Tomas' ArrayN also didn't really have utilities for growing.

[James Gallicchio]

Let me double check that though

[Mario Carneiro]

it's a primitive operation, it should be in the file

[Mario Carneiro]

While we are on the topic of simplifications to avoid unnecessary complexity, how do people feel about using this as the type of DArray:

/--
`DArray sz α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array)
with size `sz`, where the element of index `i` has type `α i`.
This type has special support in the runtime.

An array has a size and a capacity; the size is `sz` but the capacity
is not observable from lean code. Arrays perform best when unshared; as long
as they are used "linearly" all updates will be performed destructively on the
array, so it has comparable performance to mutable arrays in imperative
programming languages.
-/
structure DArray (sz : Nat) (α : Nat → Type u) : Type u where
  /-- Create a new array of size `sz` from a dependent function of type `∀ i : Fin sz, α i`. -/
  ofFn ::
  /-- A dependently typed version of `Array.get`, which returns the `i`'th element of the array. -/
  get (i : Fin sz) : α i

[Mario Carneiro]

The key point is (α : Nat → Type u) there

[James Gallicchio]

does the D in DArray stand for dynamic or dependent? I thought it was for dependent

[Mario Carneiro]

I was going to do (α : Fin sz → Type u) but I think this will just cause so much DTT hell it's not worth it, and you can recover the limited domain version using a type like fun i => if h : i < sz then α ⟨i, h⟩ else Empty

[Mario Carneiro]

It stands for dependent

[Mario Carneiro]

but I suppose the header doesn't make that obvious

[Mario Carneiro]

(This docstring is copied from Array with minor modifications)

[James Gallicchio]

you won't have any need for Fin.cons if you do Nat -> Type u :)

[James Gallicchio]

one of the applications i & tomas have for DArray is arrays indexed by FinEnum types, so honestly it's probably fine to do this and then we have the finenum indexed version which you can also use to get back Fin n version

[Mario Carneiro]

how is FinEnum defined?

[James Gallicchio]

isomorphism with Fin n for some n

[James Gallicchio]

I guess we could have DArray use FinEnum as the primitive index

[Mario Carneiro]

nope, get outta here

[James Gallicchio]

but then push is weird :)

[Mario Carneiro]

These function implementations are really beautiful

@[inline] private unsafe def setImpl (a : DArray sz α) (i : Fin sz) (v : α i) : DArray sz α :=
  unsafeCast <| Array.set (α := NonScalar) (unsafeCast a) (unsafeCast i) (unsafeCast v)

[Reid Barton]

Mario Carneiro said:

I was going to do (α : Fin sz → Type u) but I think this will just cause so much DTT hell it's not worth it, and you can recover the limited domain version using a type like fun i => if h : i < sz then α ⟨i, h⟩ else Empty

This version will also cause DTT hell because you would need to apply a theorem dif_pos inside a type to know that the type of the thing stored in the array is really given by α.

[Mario Carneiro]

yes, but the hell is limited to those cases that actually need to use Fin n there

[Mario Carneiro]

The gambit here is that in most cases, you can write down the type itself without needing the h

[Reid Barton]

I think the right approach here is to try to write the programs that want to use DArray first

[Mario Carneiro]

Fair point

[Mario Carneiro]

for something like the aforementioned FinEnum array, I am fairly confident that the DTT hell can be confined to the implementation of the wrapper itself

[James Gallicchio]

i agree, but only because you're never trying to change the size

[Mario Carneiro]

if you want to change the size and you also want Fin n functions then you will be dealing with non-defeqs in the index type no matter what you do

[Reid Barton]

I don't think this is necessarily true, is it? but then the type of push should look like
push : DArray n (α \o Fin.cast_succ) -> α \<n, _\> -> DArray (n + 1) α

[Mario Carneiro]

yes, but you will most likely have trouble making that type work in the user code

[Mario Carneiro]

α \<n, _\> is unlikely to compute nicely

[Mario Carneiro]

writing well typed functions in the DArray API isn't that hard

[Mario Carneiro]

the hard part is using those types if they are too complex

[Reid Barton]

Well if you plan to implement α \<n,h\> = f n as though the API was with Nat, you won't have to do anything special.

[Mario Carneiro]

for one thing, you will be passing f into a lot of functions by hand

[Reid Barton]

Again I think it's kind of pointless to discuss this in the abstract, rather than writing programs (not libraries)

[Mario Carneiro]

I started to write simpler-typed versions of the Fin n functions along those lines, but it does simplify a lot of the code and I'd rather wait until I see the code that needs it

[Mario Carneiro]

because DArray is already a bit out there to me

[Mario Carneiro]

but you have to write a lot of unsafe code to get a good version working, so I'm okay with centralizing that in std

[Reid Barton]

James Gallicchio said:

I guess we could have DArray use FinEnum as the primitive index

FWIW I unironically agree with this, though perhaps it should be a separate data structure (maybe one that could be implemented with DArray?)

[Mario Carneiro]

@James Gallicchio I've pushed my work to the darray branch, and I have other things I need to work on, so perhaps this is a good time to hand it off and let you work on making versions of the array definitions commented out at the end of the file.

[James Gallicchio]

Reid Barton said:

FWIW I unironically agree with this, though perhaps it should be a separate data structure (maybe one that could be implemented with DArray?)

LeanColls does the reverse of this and reimplements dynamic arrays with static sized arrays, because the unsafe primitives for static arrays are just easier to get right. There it was pointless because there's overhead reimplementing dynamic arrays built on static arrays built on dynamic arrays :joy: but maybe it would actually simplify the difficulty of getting DArray's implementation correct since you'd be able to rely on the typechecker.

I'll try continuing on the darray branch

[Tomas Skrivan]

Reid Barton said:

I think the right approach here is to try to write the programs that want to use DArray first

I strongly agree with this!

The only time when I needed something like DArray was when I wanted to iterate over all divisors of a : Nat.

My approach is to decompose a = p₁^n₁ * ... * pₖ^nₖ then define a type FinProd : List Nat → Type taking [n₁, ..., nₖ] to Fin n₁ × ... Fin nₖ. Each element of FinProd [n₁+1, ..., nₖ+1] corresponds to a divisor of a and it is easy to derive an instance of FinEnum(Enumtype in my code) so you can iterate over all the divisors.

With DArray I would have to do something like DArray ns.size (fun i => Fin (ns.getD i 0)) where ns = [n₁+1, ..., nₖ+1]. In this case it would not make a sense to do push on such DArray.

However, I can imagine that I want to work with Taylor expansions for a function f : X → ℝ. It would be a represented as an array of elements with typesℝ, X, X⊗X, X⊗X⊗X, .... Here pushing definitely makes sense.

---

I would really like to have an option to index those types in DArray either by some finite set ι(no support for pushing) or by Nat(with support for pushing). I encountered this issue when defining a type class interface for array like types, I have GenericArrayType which is an array index by some fixed type Idx and LinearGenericArrayType which defines a class of types index by Nat which supports pushing.

[Mario Carneiro]

Note that the current DArray implementation is intended to be used as a low level primitive type. You get all the same benefits and performance characteristics of Array but where the elements can all have different types. Anything beyond that sounds suitable for a library built on top of DArray, which can be done fully in safe code

[Tomas Skrivan]

Using it as a low level primitive makes sense.

[Mario Carneiro]

@Reid Barton said:

I think the right approach here is to try to write the programs that want to use DArray first

I tried it, and you were right, the (α : Nat → Type u) version doesn't work. :sad: If you try to build the (α : Fin sz → Type u) version on top of it you get stuck in those fun i => if h : i < sz then α ⟨i, h⟩ else Empty situations needing a theorem that says (∀ i < sz, α i = α' i) → DArray sz α = DArray sz α', which isn't provable. I reverted the darray branch to use (α : Fin sz → Type u) instead, and added some abbreviations for the more common cases:

/--
`DArray sz α` is the type of (dependently typed)
[dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array) with size `sz`,
where the element of index `i` has type `α i`. This type has special support in the runtime.

An array has a size and a capacity; the size is `sz` but the capacity
is not observable from lean code. Arrays perform best when unshared; as long
as they are used "linearly" all updates will be performed destructively on the
array, so it has comparable performance to mutable arrays in imperative
programming languages.
-/
structure DArray (sz : Nat) (α : Fin sz → Type u) : Type u where
  /-- Create a new array of size `sz` from a dependent function of type `∀ i : Fin sz, α i`. -/
  ofFn ::
  /-- A dependently typed version of `Array.get`, which returns the `i`'th element of the array. -/
  get (i : Fin sz) : α i

/--
An abbreviation for `DArray` in the special case where `α` is defined for all `i : Nat`, not
just `i : Fin sz`.
-/
abbrev DNArray (sz : Nat) (α : Nat → Type u) := DArray sz (α ·)

/--
An abbreviation for `DArray` in the special case where `α` is actually a constant. This is similar
to (and interconvertible with) `Array α`, except that `sz` is part of the type.
-/
abbrev CArray (sz : Nat) (α : Type u) := DArray sz fun _ => α

[James Gallicchio]

@Mario Carneiro I have some time now to work on the commented out section if your updates are pushed

[James Gallicchio]

Is it alright if I make functions like modifyM take Fin sz instead of Nat? or was your goal to preserve the Array API as close as possible?

[James Gallicchio]

I think for modify I will since I can't imagine wanting the function to have any type other than α i → α i

[James Gallicchio]

Another note -- I agree that the common use case is for α to remain constant across most operations where sz is constant, but I also have applications in mind where α is updated at individual indices, and I'm not sure how we plan to support that

[James Gallicchio]

(though, that's how you get into DTT hell... :pensive: not really sure what to do about it)

[Mario Carneiro]

James Gallicchio said:

Is it alright if I make functions like modifyM take Fin sz instead of Nat? or was your goal to preserve the Array API as close as possible?

The pattern I have been following is that anything that does not necessarily require its input to be in bounds is translated to a DNArray function, and there should also be a version which has required inbounds and uses DArray

[Mario Carneiro]

See e.g. get / getD / get!

[Mario Carneiro]

I don't have a great naming suggestion though, maybe modifyM' for the out of bounds version

[James Gallicchio]

well, this goes to my general grievance that we should stop with this unnecessary get/getD/get! name pollution and just return Partials with Partial.! and Partial.orDefault etc defined...

[James Gallicchio]

but this is not the place to argue about that

[Mario Carneiro]

indeed

[Mario Carneiro]

I think you are describing the Option type, and we already have that

[James Gallicchio]

We should make a separate thread, actually, since it's probably worth discussing

[Mario Carneiro]

But it is very important here to preserve the performance characteristics of the array functions. Only zero cost operations are allowed over the original array function

[Mario Carneiro]

returning thunks is not an option, if that's your proposal

[James Gallicchio]

James Gallicchio said:

Another note -- I agree that the common use case is for α to remain constant across most operations where sz is constant, but I also have applications in mind where α is updated at individual indices, and I'm not sure how we plan to support that

@Mario Carneiro did you have thoughts about this? Many of the functions could be duplicated with Function.update-esque versions.

[Mario Carneiro]

yes, that sounds fine

[James Gallicchio]

maybe with names like dSet/dModify?? best I could come up with

[Mario Carneiro]

they won't be the "default" version, of course, and we'll need a new naming convention for them. setU?

[James Gallicchio]

what does the U stand for?

[Mario Carneiro]

update

[Mario Carneiro]

I have heard this referred to as "strong update"

[James Gallicchio]

ehhhhhhhhhh i don't love it but I see the justification

[Mario Carneiro]

that is to say, an assignment that changes the type of the referent

[James Gallicchio]

sSet (strong set) has the advantage of being a homophone with ß

[Mario Carneiro]

ßet

[James Gallicchio]

:b:et

[Mario Carneiro]

I think it would be sset if we want that name

[James Gallicchio]

I could get behind setS. I wish ...D weren't taken up as shorthand for ?.getD, so that we could have D stand for dependent.

[Mario Carneiro]

I'm not sure dependent is a good name though, everything is dependent

[James Gallicchio]

yeah

[Mario Carneiro]

of course it doesn't have to be abbreviated, e.g. strongSet

[James Gallicchio]

let me see if agda has a dependent array implementation somewhere

[James Gallicchio]

what about H for heterogeneous?

[James Gallicchio]

a la heterogeneous lists

[Mario Carneiro]

that's no better, that's just a synonym for dependent

[Mario Carneiro]

plus it is made worse by the fact that heterogeneous is used to mean other things in lean

[James Gallicchio]

(it is?!)

[Mario Carneiro]

HAdd, HEq

[James Gallicchio]

oh, but those fit the notion that heterogeneity = types are not all the same across the operation

[Mario Carneiro]

which... isn't what is happening here

[James Gallicchio]

in this case, the returned array does not have the same type as the argument array

[Mario Carneiro]

that's already true of the regular push

[James Gallicchio]

yeah. but push doesn't have a non-heterogeneous analog :stuck_out_tongue:

[Mario Carneiro]

I'm going to make an executive decision and say strongSet for this (and strongModify, strongSwap etc). It's a long name but it will get people to read the docs

[Mario Carneiro]

Either that or we can make a poll

[James Gallicchio]

it seems fine to me

[James Gallicchio]

oh, Function.update is in mathlib. hm

[James Gallicchio]

I will delta expand for now, but I'm not sure if that has consequences for simp-ability

[Mario Carneiro]

move Function.update

[Mario Carneiro]

Std.Data.Function.Basic

[James Gallicchio]

separate PR?

[Mario Carneiro]

this isn't a PR yet

[James Gallicchio]

sure, just making sure you don't mind having upstreamed stuff in the branch :)

[Mario Carneiro]

I did Fin.Basic on the branch before rebasing / merging it to main

[James Gallicchio]

std4#168

[James Gallicchio]

There's a cast in modifyM because I didn't feel like implementing it twice just to avoid the cast. But that might make proofsing a pain.

[Mac Malone]

Mario Carneiro said:

I'm going to make an executive decision and say strongSet for this (and strongModify, strongSwap etc). It's a long name but it will get people to read the docs

What about setT (where T stands for type), since what this is doing is setting a value and updating the type? I would say those are rather long and not very informative names (the terms strong and weak generally have to do with including or excluding some check, which, imo, is something of a stretch here).

[James Gallicchio]

strongSet grew on me tbh

[James Gallicchio]

but we can poll if u want

[Mario Carneiro]

Mac said:

(the terms strong and weak generally have to do with including or excluding some check, which, imo, is something of a stretch here)

I don't think there is precedent for such meaning of the words strong and weak in lean

[Mario Carneiro]

the usage of strong in mathlib seems to follow the general pattern:

• On nouns / types: an object with more properties than usual
• On verbs / functions: an operation with fewer restrictions in the hypothesis or more properties in the consequent

In this sense strongSet uses the "fewer restrictions on hypotheses" reading

[Reid Barton]

My feeling is that this use of strong here will not make sense to anyone else, but I also don't have a better alternative to suggest.

[Mac Malone]

Mario Carneiro said:

I don't think there is precedent for such meaning of the words strong and weak in lean

I was refering to the more general CS senses of terms (e.g., strong and weak references / pointers, strong and weak symbols, etc.)

[Reid Barton]

In Haskell, these kind of operations are called "type-changing update"

[Mac Malone]

Mario Carneiro said:

In this sense strongSet uses the "fewer restrictions on hypotheses" reading

I think it is quite a stretch to call changing the type "fewer restrictions on hypotheses". This is a mutation action that mutates more than just the value but also the type (EDIT: as Reid said above). It has about as much to do with hypotheses as the difference between a pure vs monadic function (i.e., it can be phrased that way, but that is not exactly the natural intuition). I think Lean's notion of heterogeneity is closer to what is going on here than strength.

[James Gallicchio]

setAndChangeType (long name discourages use, which is desirable here)

[Mac Malone]

@James Gallicchio I am still not sure I understand what is rational for discouraging use. A type-heterogenous mutable array seems like a generally useful alternative to the very memory-inefficient tuple product for many-element use cases.

[James Gallicchio]

it's a dangerous operation because it introduces Function.update in the type, which frequently has to be cast through. The common case for this type is to have different types at each index, BUT to not change those types ever. Changing the types is a pretty rare use case as far as I understand.

[Mac Malone]

One use case for such a DArray that immediately stands out to me is for the child nodes of a provably-correct AST parser.

[Mac Malone]

Which, in the case of syntax transformations (e.g. macros) or the like very well my undergo type changing mutations.

[Mac Malone]

James Gallicchio said:

which frequently has to be cast through

I remember you mentioning this before. What is the problem with cast? I have found it quite useful in Lake, but maybe I am doing things wrong?

[James Gallicchio]

it's just hard to get rid of a cast when trying to prove anything about an expression that has a cast in it. I think it's usually recommended to hide the cast behind a def, and have specialized lemmas for rewriting the definition without introducing the underlying cast to the expression.

[James Gallicchio]

if you don't care about proving anything then it is ~never an issue

[Mac Malone]

That sill confuses me. Isn't cast h a provably equal to a (or, more accurately cast h.symm (cast h a) = a)? Isn't that the whole point of cast?

[James Gallicchio]

only if the equality h can be dependently eliminated. which can be a big issue once your types get nontrivial.

[Mac Malone]

@James Gallicchio I'm sorry, what does "dependently eliminated' mean here? (Sorry, I should probably know this.)

[James Gallicchio]

for all i know it could be a source of incompleteness in Lean; there's been times when i had a cast in my goal and simply couldn't proceed after bashing my head at it, until I gave up and redesigned everything to avoid casting :man_facepalming:

[James Gallicchio]

Mac said:

James Gallicchio I'm sorry, what does "dependently eliminated' mean here? (Sorry, I should probably know this.)

I think it's roughly that there's some substitution of variables in the context such that the equality is defeq??? but someone should fact check me

[James Gallicchio]

i know v = f x can be dependently eliminated by substituting [f x / v], while f x = g y generally can't be eliminated :P

[James Gallicchio]

definitely worth trying to prove some stuff with casts in it. the frustration left quite an impact on me

[Mac Malone]

Oh, giving the basic example I wrote above cast h.symm (cast h a) = a a try, I think I might understand where the problem comes. Since type equality/inequality is generally independent of Lean's theory, proving things about casts likely requires more axioms (just like proving things about types often does). Thus, doing so poses the risk of introducing inconsistent into the axiom set of Lean.

[Sebastian Ullrich]

That should be cases h; rfl

[James Gallicchio]

well the thing is all casts can be proven propositionally to be correct, cuz you have the proof h. so the type equality given by h is always provable in Lean DTT. but the cast can only be eliminated if it's defeq, which is obviously much more restrictive. Usually I think you can turn a propositional equality into a definitional one by carefully generalizing the goal, but I don't know how to always do it in general (or whether it's always possible)

[Mac Malone]

Yep, that does work here. But I realized through the effort that the type equality of cast is probably often hard to eliminate and that it does not help you determine what the constructed result of the cast is in the target type.

[Mac Malone]

The simplest, general way to perform this elimination does seem like it might be by a reverse cast.

[Mac Malone]

Or by usual general solutions that can treat it as a variable e.g. induction on the result.

[James Gallicchio]

yep. but if the cast term is an argument to another function (a common case) then you can't just apply the reverse cast on both sides, and if the type is parametric you can't induct on it. so it's very very easy to hit a case where something just becomes very difficult to prove. thus, lots of lemmas to circumvent introducing cast in the goal!

[Mac Malone]

The reverse cast is probably sufficient for my example use cases in Lake where casting is mediated by an opaque type in between so all casts are essentially guaranteed to have both a to and and a from (e.g., toFamily/ofFamily for Lake's open types).

[Mac Malone]

I imagine this might even be more generally true for many dependent data-structure use cases of cast, where you often cast to some unwieldy type on a set (e.g., the \b function of Lake's DRBMap or the \a function of a DArray) and then cast back from it on a get.

[James Gallicchio]

anyways, let's do a poll!

[James Gallicchio]

/poll What to name the type-changing set function? (and other modifying operations)
strongSet (a stronger operation!)
setStrong (an operation, but stronger!)
setT (Typechanging)
setH (Heterogeneous)
setAndChangeType (descriptive!)
setPoly (now with extra polymorphism)

[Mac Malone]

@James Gallicchio If we do lean towards the descriptive setAndChangeType, I wonder if we could go for something a bit shorter like setWithType. (I will add it to the poll, but it may be a bit late as people have already voted.)

[Reid Barton]

I am actually curious to hear any practical application of dependent arrays.

[Mac Malone]

@Reid Barton My example above was for the children of (provably) well-formed nodes of a syntax tree.

[Reid Barton]

Why not use a structure?

[James Gallicchio]

My application is to have a concrete/efficient implementation of (i : Fin n) -> tau i.

[Reid Barton]

I understand that much of course but what is tau, i.e., what is it for.

[Reid Barton]

I've never used a language that had dependent arrays so I can't easily think of problems where they would be useful.

[James Gallicchio]

right now in a project I have

structure Coords (sz : Dim → Nat) where
  val : FIArray Dim Nat
  hval : ∀ d, val[d] < sz d

where FIArray is a finenum-indexed array and Dim is FinEnum. I had to write a bunch of wrapper functions to convert to/from Fin (sz d) which was a pain.

[Mac Malone]

Reid Barton said:

Why not use a structure?

A couple of reasons:

1. The well-formedness may be layered over an existing simple representation (e.g., Lean's Syntax)
2. You would need a structure for each node kind and an inductive to wrap them all up, but that inductive may be impossible to construct if syntax can be defined lazily (like in Lean).
3. Since the syntax can be built up step-by-step by sequential parsers, you need some representation for the intermediate steps. A well-formed heterogenous array seems like the best option there.

[Reid Barton]

Yes the main example that comes to mind is that you have a different predicate on each element of an array of some plain type. I'm not convinced it isn't better dealt with in the way you already have.

[Kyle Miller]

@Reid Barton They could be useful for randomly sampling pi types (setup: the domain is a FinEnum and each fiber is sampleable), and you need some kind of data to store the sampled values per index. It could be done as an array of sigma types, but (1) you don't really need to store the pairs since you know from the pi type what the types are supposed to be and (2) it might be useful having an API deal with dependent type issues from indexing and inferring the elements have the expected type.

[Mac Malone]

Reid Barton said:

I'm not convinced it isn't better dealt with in the way you already have.

I do not know what you mean by this? What way?

[Reid Barton]

Exactly as an ordinary array combined with a proof about each element of the array.

[James Gallicchio]

I also want to use them in combination with the fully under-defined type Uninitto have partially-initialized arrays as a primitive, which is a pretty neat use. Something like:

@[implemented_by Darray.uninitUnsafe]
def DArray.uninit (n) : DArray n (fun _ => Uninit) := ...

I think this is a notable example because you sorta can't do it as a structure without introducing some overhead in the form of sigma types (as Kyle brought up).

[Mac Malone]

Reid Barton said:

Exactly as an ordinary array combined with a proof about each element of the array.

Isn't essentially what DArray is? An array with a known size and function predicate that provides proof about the type of each element of the array?

[Reid Barton]

Not really; for example the first element of the array might be a float and the second one might be a function.

[James Gallicchio]

I think Reid's point is that if the elements are all subtypes of the same concrete type then there's other simple ways to do it.

[James Gallicchio]

But I think there's enough examples where this genuinely saves overhead, and I also think not having to reimplement functions to get into and out of subtypes is nice.

[Mac Malone]

@James Gallicchio Oh, I'm curious, what would be the simpler solution?

[Reid Barton]

I think Kyle's example makes sense to me though.

[James Gallicchio]

Mac said:

James Gallicchio Oh, I'm curious, what would be the simpler solution.

https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/Fin.20basics/near/372694622

[Mac Malone]

@James Gallicchio I am not seeing how that example translates to my use case.

[James Gallicchio]

It doesn't. There are applications where this doesn't work (i.e. when your array is not subtypes of the same type).

[Mac Malone]

@James Gallicchio My question is, I still don't see how that translates even when they are of the same type.

[Mac Malone]

How would I use that provide a different subtype predicate about each element of an array? For instance, for the simple syntax "a + b" where arr[0] and arr[2] are ident subtypes of Syntax, ar[1] is a + atom subtype of Syntax.

[James Gallicchio]

You can parametrize by a indexed predicate P : Fin n -> tau -> Prop and require that P i backing[i] for all i, if that makes sense.

[James Gallicchio]

In your case tau = Syntax and P describes the type of all the syntax objects.

[Mac Malone]

James Gallicchio said:

You can parametrize by a indexed predicate P : Fin n -> tau -> Prop and require that P i backing[i] for all i, if that makes sense.

True, but that does mean I just have to write my own custom Array type to support this (backed by Array), which seems mighty inconvenient as opposed to a general case already supported by Std.

[Reid Barton]

Right so in this case the "raw" data is Syntax, rather than Array Nat or whatever. The generic version of the approach is to "store" a proposition stating that the data is "well-formed" alongside the raw data, rather than baked deeply into its type.

[Reid Barton]

One concrete advantage is that it's much more efficient when you have to cross a boundary between working with well-typed vs. raw data (since you don't have to copy the actual data part), or considering different amounts of well-formedness.

[Mac Malone]

Reid Barton said:

Right so in this case the "raw" data is Syntax, rather than Array Nat or whatever.

While this is true generally, this does not work while constructing the Syntax. The parser will build up an well-formed array of syntax that it will then convert into a well-formed Syntax.node. In order to create that well-formed node, the Array needs to carry proofs that its elements are proper constituents (and those elements themselves need to carry the information that they are well-formed).

[Mac Malone]

To me, the most obvious way to do this is to have some Node typeclass that constructs a well-formed node from a DArray-like well-formed array of children that was built up by the parser combinators.

[Reid Barton]

It should work fine. The parser also simultaneously builds a proof that the Array is well-formed and then this proof is returned together with the Syntax to the parent node which uses it to build its own proof of well-formedness, recursively.

[Mac Malone]

Reid Barton said:

The parser also simultaneously builds a proof that the Array is well-formed,

How is building an array with a proof significantly different / more user-friendly than just building a DArray (or the like)?

[Mac Malone]

E.g., the parser combinators still need to carry this information in the type because the components do not know what kind of node they are building only that they are building an array and that its elements are well-formed version of whatever type of syntax (e.g., Ident, NumLit, etc.).

[Mario Carneiro]

You can still wrap that pair of (untyped data, well formedness proof) into a new type and have your parser combinators manipulate it as a unit

[Mario Carneiro]

the point is that afterwards you get more flexibility to change the proof to a different kind of well formedness proof or get at the untyped data without having to deep copy everything

[Mario Carneiro]

@Reid Barton While looking into lake refactoring stuff, I noticed that Mac is using a dependent hashmap in a fairly essential way. I'm curious what you think about it. The main "entry point" is here, it's storing a map where key n : Name maps to an opaque family F n : Type. This is later manipulated by using axioms of the form axiom : F `foo = Nat, axiom : F `bar = IO Unit etc which are declared on the fly using (things that unfold to) the family_def macro, e.g. here

[Mac Malone]

Mario Carneiro said:

You can still wrap that pair of (untyped data, well formedness proof) into a new type and have your parser combinators manipulate it as a unit

Yeah, I agree with that. The problem is building up an array of those (untyped data, well formedness proof) type units. James suggestion of (untyped data array, well formed proof predicate) seems like the correct solution also. My understanding is that later combo is much the same as DArray except DArray is more general. Thus, using DArray seems better than just rolling one's own. Maybe I misunderstood somewhere?

[Mario Carneiro]

you wouldn't build up an array of such directly, you would unpack the data and the proof, array up the data and make a composite proof depending on the array

[Mac Malone]

@Mario Carneiro Huh? I do not get what you mean by that.

[Mario Carneiro]

In the end you get something with roughly the same API as an intrinsically dependently typed version, but it is actually implemented to bubble out all the proof stuff separate from the data

[Mario Carneiro]

maybe you can give a concrete example and I can demonstrate?

[Mario Carneiro]

Note that this technique is limited to cases where the actual data is uniformly typed, while DArray handles the case where each element is a different type. But this is a rare use case and it's one of the reasons lean has a crappy ABI in the first place so I think we would want to avoid it in the long term

[Mac Malone]

Here is a simplified pseudocode example:

def Ident := {stx : Syntax // stx.isIdent}
def Plus := {stx : Syntax // stx = .atom "+"}

def WfAdd (stx) := stx = .node `add args /\
  args.size = 3 /\ args[0].isIdent /\ args[1] = .atom "+" /\ args[2].isIdent
def Add := {stx : Syntax // WfAdd stx }
def WfNode : Name -> Syntax -> Prop
| `add => WfAdd
| - ...

def Node (k : Name) {stx : Syntax // WfNode k stx}
class MkNode (kind : Name) (args : A) where
   mkNode : A -> Node kind

instance : MkNode `add (Ident X Plus X Ident) where
  mkNode ((lhs, hl), (plus, hp), (rhs, hr)) :=  (.node `add #[lhs, plus, rhs], by ...)

instance : HAndThen  (Parsec A) (Parsec B) (Parsec (A X B)) where
  hAndThen p1 p2 := (<- p1, <- p2 ())

def ident : Parsec Ident := -- ...
def plus : Parsec Plus := -- ...
def add : Parsec Add :=
  mkNode `add (ident >> plus >> ident)

[Mario Carneiro]

there are some missing imports, I get errors all over the place

[Mac Malone]

Hence "pseudocode" :wink:

[Mac Malone]

If you want, I can work on making a proper #mwe, but I'll probably post that tomorrow.

[Mario Carneiro]

here's my closest attempt at a MWE version

open Lean (Name)
namespace Foo

inductive Syntax : Type
| atom (_ : String)
| node (_ : Name) (_ : Array Syntax)
deriving Inhabited

axiom Syntax.isIdent : Syntax → Bool

def Ident := {stx : Syntax // stx.isIdent}
def Plus := {stx : Syntax // stx = .atom "+"}

def WfAdd (stx : Syntax) := ∃ args, stx = .node `add args /\
  args.size = 3 /\ args[0]!.isIdent /\ args[1]! = .atom "+" /\ args[2]!.isIdent
def WfNode : Name → Syntax → Prop
| `add => WfAdd
| _ => fun _ => False

def Node (k : Name) := {stx : Syntax // WfNode k stx}
def Add := Node `add
class MkNode (kind : Name) (A : Type) where
   mkNode : A → Node kind
open MkNode (mkNode)

instance : MkNode `add (Ident × Plus × Ident) where
  mkNode | (⟨lhs, hl⟩, ⟨plus, hp⟩, ⟨rhs, hr⟩) => ⟨.node `add #[lhs, plus, rhs], sorry⟩

def Parsec : Type → Type := sorry
instance instMonadParsec : Monad Parsec := sorry

instance : HAndThen (Parsec A) (Parsec B) (Parsec (A × B)) where
  hAndThen p1 p2 := return (← p1, ← p2 ())

def ident : Parsec Ident := sorry
def plus : Parsec Plus := sorry
def add : Parsec Add :=
  mkNode <$> (ident >> plus >> ident)

[Mario Carneiro]

That's pretty good, but I would structure it a bit more like this:

open Lean (Name)
namespace Foo

inductive Syntax : Type
| atom (_ : String)
| ident (_ : String)
| node (_ : Name) (_ : Array Syntax)
deriving Inhabited

inductive Syntax.IsIdent : Syntax → Prop
  | mk (s) : IsIdent (.ident s)

inductive Syntax.IsAtom (k : String) : Syntax → Prop
  | mk : IsAtom k (.atom k)

inductive Syntax.IsExpr : Syntax → Prop
  | ident : IsIdent stx → IsExpr stx
  | add : IsExpr a → IsAtom "+" b → IsExpr c → IsExpr (.node `add #[a, b, c])

def Ident := {stx : Syntax // stx.IsIdent}
def Atom (k) := {stx : Syntax // stx.IsAtom k}
def Expr := {stx : Syntax // stx.IsExpr}

instance : Coe Ident Expr := ⟨fun ⟨stx, h⟩ => ⟨stx, .ident h⟩⟩

def Parsec (A : Type) : Type := String → (sorry : Type)
instance : Inhabited (Parsec A) := sorry
instance : Monad Parsec := sorry
instance : Alternative Parsec := sorry

instance : HAndThen (Parsec A) (Parsec B) (Parsec (A × B)) where
  hAndThen p1 p2 := return (← p1, ← p2 ())

def str : Parsec String := sorry
def atom (k) : Parsec (Atom k) := sorry
def ident : Parsec Ident := do let s ← str; return ⟨_, .mk s⟩
partial def expr : Parsec Expr :=
  (return (← ident : Expr)) <|>
  (return ⟨_, .add (← expr).2 (← atom _).2 (← expr).2⟩)

[Mac Malone]

@Mario Carneiro Cool! :tada: However, that version does not use >> for joining parsers, which is a major disadvantage when e.g. translating from syntax.

[Mario Carneiro]

It is possible to write an instance to make >> work, I just didn't see the point because it involves an extra MkNode instance that is used in exactly one place, so my instinct is to not create a useless indirection. Ideally, if you were translating from syntax, there would be a macro that just mines the declarations themselves to construct both the inductive type IsExpr as well as the expr parser. If it's being done manually, I think one line for the inductive and one line for the parser is a quite reasonable overhead. Maintaining syntactic parity with the untyped formulation wasn't really a goal in the first place.

[Mac Malone]

@Mario Carneiro I can understand that logic. Obviously, in a real example, there would be more than one node kind and nodes may also be constructed manually outside the parser, so the MkNode is more useful. One thing I did notice while looking through the example more is that this assumes the syntax of a well-formed entirely determined by its well-formedness. In a real example, the syntax would also have non-determined information (e.g., SourceInfo), so the code would still need to construct the array as well as the proof in the node -- making the lack of utilities like >> more inconvenient.

[Mario Carneiro]

The presence of SourceInfo is actually exactly why I wrote it with IsAtom k which is just a singleton instead of inlining .atom "+" for b in IsExpr.add

[Mario Carneiro]

there can be other arguments to the function determined by other monadic things

[Mario Carneiro]

I am not sure of the details since Parsec isn't defined in this MWE

[Mac Malone]

@Mario Carneiro Just FYI, I was using Parsec to invoke something e.g. Lean.Data.Parsec-like.

[Mario Carneiro]

I know

[Mario Carneiro]

but the details affect how exactly you would write these things

[Mario Carneiro]

or what is the least cumbersome thing

[Mac Malone]

Makes sense.