N-Ary Tuple

Stream: lean4

[Paul Mure]

Hi,

I am designing an embedded DSL for writing hardware accelerators in Lean4 with an approach based on Fe-Si.

I need to have an n-ary tuple as a primitive type in my object language like so:

inductive Ty where
  | unit
  | bool
  | uint32
  | tuple   : List Ty → Ty
  ...

I'm stuck on how to proscribe denotational semantics to the tuple type.

My approach was to use a heterogenous list as described in this example like so:

@[reducible] def Ty.denote : Ty → Type
  | unit            => Unit
  | bool            => Bool
  | uint32          => UInt32
  | tuple tys       => HList Ty.denote tys

However, Lean cannot prove that this function terminates even though it indeed does since HList will only every call denote on the elements of tys.

I also tried creating a wrapper around the built-in binary product type but cannot figure out how to do so in a way that works with the denote function.

Thanks for any help in advance!

[Reid Barton]

Here is one option. I'm not sure how well this works in practice. In Lean 3 the general wisdom was that it was better to implement nested inductive types yourself, to get better control/visibility of the actual definitions.

@[reducible] def Ty.denote : Ty → Type
  | unit            => Unit
  | bool            => Bool
  | uint32          => UInt32
  | tuple tys       => go tys
where
  go : List Ty → Type
  | [] => Unit
  | ty :: tys => ty.denote × go tys

[Reid Barton]

"implementing nested inductive types yourself" here would mean defining mutual Ty, ListTy types

[Reid Barton]

Personally I would try to avoid List and instead only support binary products, or encode lists as functions

[Paul Mure]

Reid Barton said:

Personally I would try to avoid List and instead only support binary products, or encode lists as functions

The problem with binary products is that accessing an element from an n-ary tuple now can take log(n) steps instead of one step with a flat encoding. While it might be possible to optimize that in a later stage, a first-class support for n-ary tuple would make things easier.

[Reid Barton]

Oh I would have guessed that all your data is unboxed/flat, in which case everything is constant time.

[Paul Mure]

We still want to support nested tuples, so enforcing every tuple to be flat will be suboptimal.

[Reid Barton]

You can also consider having an unboxed tuple, and a "box".

[Paul Mure]

Would you mind going into a little more details?

[Reid Barton]

Well you already have the unary case of your tuple, which I infer would be implemented as a pointer.

[Reid Barton]

With that and an unboxed pair you can build all the other cases of your tuple.

[Reid Barton]

I personally wouldn't build anything serious on top of nested inductive types (List Ty -> Ty) since it is the sort of thing where months later you will discover that it isn't supported very well by whatever you need and it will be too late to change everything.

[Paul Mure]

Our DSL is meant to be a high-level hardware description language, so there's really no concept of pointers and boxed values as in low-level software.

But I agree that nested inductive types like these could create other unnecessary headaches down the line. So it seems like binary tuples are the way to go and we will worry about optimizing accesses as a later compiler pass.

Thanks a lot for your input!

[Reid Barton]

(Just to be explicit, I'm assuming from context that you want to use these nested inductive types in a theorem proving setting, e.g., for a verified compiler. If you only need them in a programming setting, then they are totally fine because Lean itself uses them heavily.)

[Paul Mure]

Reid Barton said:

(Just to be explicit, I'm assuming from context that you want to use these nested inductive types in a theorem proving setting, e.g., for a verified compiler. If you only need them in a programming setting, then they are totally fine because Lean itself uses them heavily.)

Yes, every language construct will be used heavily in a theorem proving context.