Compile the 'unit' type as a zero-size value

[athas]

The core language uses a special cert scalar type for tracking variables where the value doesn't matter, but only the data dependency. In particular, this is used to ensure bounds checks occur before the index operations they protect. It is possible for arrays of cert to exist, and these then end up being compiled as arrays of bytes. It would be better if we treated cert to have a size of zero bits, meaning that arrays of them would take no space. If we then also translated empty tuples to certs, then we could use [n]() as a type witness for the size n with zero overhead.

[henglein]

Sounds like phantom types and their implementation.

On Mon, Feb 15, 2021 at 11:24 PM Troels Henriksen notifications@github.com wrote:

The core language uses a special cert scalar type for tracking variables where the value doesn't matter, but only the data dependency. In particular, this is used to ensure bounds checks occur before the index operations they protect. It is possible for arrays of cert to exist, and these then end up being compiled as arrays of bytes. It would be better if we treated cert to have a size of zero bits, meaning that arrays of them would take no space. If we then also translated empty tuples to certs, then we could use [n]() as a type witness for the size n with zero overhead.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fdiku-dk%2Ffuthark%2Fissues%2F1255&data=04%7C01%7Chenglein%40di.ku.dk%7C514f0da8c1684c28c20908d8d2007094%7Ca3927f91cda14696af898c9f1ceffa91%7C0%7C0%7C637490246615062617%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=GGZoNJmdr247uLzVpthr5p3TuJnmEwBV9DUIa%2BHTxSw%3D&reserved=0, or unsubscribe https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAAFDZD3FPPNCL4XS6DVS7Z3S7GNJFANCNFSM4XVMWAJA&data=04%7C01%7Chenglein%40di.ku.dk%7C514f0da8c1684c28c20908d8d2007094%7Ca3927f91cda14696af898c9f1ceffa91%7C0%7C0%7C637490246615062617%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=P52Nd5MTJ6oIwjLaO97fjw7vqVJM1QeHOWCPDe2%2BGAE%3D&reserved=0 .

-- Fritz Henglein fritz@henglein.com +45-30589576

[athas]

Not exactly; phantom types already work in Futhark, but in most languages they don't carry any values and are gone at runtime, and typically also in the compiler IR. We actually need to carry these certs around to enforce "fake" data dependencies all the way to final code generation. In the case of [n](), we must carry the integer n around at runtime as well, since it is in scope in the term language.

[henglein]

Phantom types are parametric types that capture dependencies in the sense that they could contain any number of elements, but since they are pure sets (no operations such as equality test elements are used on their elements), they can be implemented by the empty type (which requires zero bits). I thought that's what you were doing. If you need the exact value of the integer n to do something with 'destructively -- observe not, not just copy/refer to it -- (as I had gotten the impression of), it's not a phantom type, but some type with those operations. (I don't know what you mean by being 'in scope' the term language -- the trick with phantom types is that they can occur and be in scope all over the place, but require zero bits and no operations anyway.) If its something that's parametrically pulled around and only at the end 'discovered' to be an integer, it sounds like it is parametric, like a phantom type, but where the instantiation is a specific one, not just any one.

F

On Tue, Feb 16, 2021 at 10:14 AM Troels Henriksen notifications@github.com wrote:

Not exactly; phantom types already work in Futhark, but in most languages they don't carry any values and are gone at runtime, and typically also in the compiler IR. We actually need to carry these certs around to enforce "fake" data dependencies all the way to final code generation. In the case of [n](), we must carry the integer n around at runtime as well, since it is in scope in the term language.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fdiku-dk%2Ffuthark%2Fissues%2F1255%23issuecomment-779696256&data=04%7C01%7Chenglein%40di.ku.dk%7C76b1573b56ef40253c2708d8d25b4a94%7Ca3927f91cda14696af898c9f1ceffa91%7C0%7C0%7C637490636818407478%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=ansnL1IuyWtW%2BsHbhkHS6WvmqNVZrdhZaGV7ds8wZ5Y%3D&reserved=0, or unsubscribe https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAAFDZD5AOYH7GLDUKV363IDS7IZP7ANCNFSM4XVMWAJA&data=04%7C01%7Chenglein%40di.ku.dk%7C76b1573b56ef40253c2708d8d25b4a94%7Ca3927f91cda14696af898c9f1ceffa91%7C0%7C0%7C637490636818407478%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=2ASqEOInXVqaP8FSpy673zys4EAp%2FSM7cScW56ff4ns%3D&reserved=0 .

-- Fritz Henglein fritz@henglein.com +45-30589576

[athas]

Hm, if we want to serialise these things, we also need to extend the binary data format with a new primitive type... for the first time in many years. I guess there's no way around it.