On: How Integers Should Work (In Systems Programming Languages)

[Peaker]

To add 100 to a pointer, you would need a pointer to an allocation of at least 100 bytes.

Thus, your pointer would have a type that provides evidence that it points to at least 100 bytes. This would make pointer arithmetic adding 100 bytes possible. Something like:

  addPtr :: Address (size : Nat) -> (x : Fin size) -> Address (size - x)

[Someone → Peaker]

Wouldn't that better be:

  addPtr :: Address (presize : Nat, size : Nat) -> (x : Fin size) -> Address ( presize + x, size - x)

presize = number of 'slots' available before the current value.

size = number of 'slots' available after the current value.

That would allow for later subtraction, too.

[Peaker → Someone]

Yes, indeed :-)

I did not mean to write an actual implementation, just to make a small point.

In an actual implementation, I'd probably want the type to convey information about the content stored at the address, too.

[scott_s → Peaker]

Can you explain the semantics of that notation? I can glean some of its meaning, but I'd like to understand it in full.

[Peaker → scott_s]

    addPtr : Address (size : Nat) -> (x : Fin size) -> Address (size - x)

(the :: above should have been a single colon) Reads as:

   "addPtr" is a value of the following type:

Function from two args: "Address (size : Nat)" and "(x : Fin size)" to result "Address (size - x)"

"Address (size : Nat)" is the "Address" type applied to one Natural number parameter named "size" (indicating the allocation size the value of that Address points at).

(x : Fin size) means it takes an "x" of type "Fin size". The "Fin param" type is a type that can hold a natural number 0..param-1. The resulting Address has a smaller size it points at.

[Locke1689 → Peaker]

Ah, very clever construction, I like it. Thanks for the input.

[doublec → Locke1689]

ATS has similar constructs. Once you have allocated memory you can't do pointer arithmetic outside the bounds of the size of the memory allocated, checked at compile time.