Zulip Chat Archive

Stream: lean4

Topic: Fixed precision signed integer types

Cole Shepherd (Dec 05 2022 at 05:41):

Does Lean 4 have fixed precision signed integer types? I see types like UInt8 and UInt32, but no corresponding signed types.

Chris Bailey (Dec 05 2022 at 05:44):

I have an implementation here but there aren't signed integers in core/std yet.

Cole Shepherd (Dec 05 2022 at 06:12):

Is this on the roadmap for core/std?

Mario Carneiro (Dec 05 2022 at 07:06):

That has to be in core, because the operations need a primitive implementation

Kevin Buzzard (Dec 05 2022 at 07:27):

Conversely I thought that the idea of core was that it contained only the things needed to implement core?

Mario Carneiro (Dec 05 2022 at 07:29):

It contains things that need support / integration with the runtime and/or compiler

Mario Carneiro (Dec 05 2022 at 07:30):

obviously the compiler should know about your signed integer type so it can do e.g. constant propagation

Mario Carneiro (Dec 05 2022 at 07:31):

and it may or may not warrant support in the ABI as well, seeing as C has signed integer types

Henrik Böving (Dec 05 2022 at 16:40):

I actually designed the new constant folder to allow users to add their own folders. In theory any library can inject their own constant folder for their own numeric types without issues so thats not a blocker.

The other reason I can see would be that we might want to translate them to C types as you mentioned. But as mentioned in previous meetings I was hoping that ideally we might figure out a general way to have custom c integer types addable from outside the compiler.

Tomas Skrivan (Dec 05 2022 at 16:51):

What is Chris Bailey's approach missing? If I understand it correctly, his integers will be unboxed if possible, right? However, I'm not 100% sure what is constant propagation doing and that might be the problematic part.