5 ms·

This is interesting but I've never seen a dependent type system (even Coq) that can do this completely. For example, let's say I'd like to turn a pointer into a

This is interesting but I've never seen a dependent type system (even Coq) that can do this completely. For example, let's say I'd like to turn a pointer into an integer (a reasonably common systems operation) so I define a type addr bounded between 0 and 2^32-1. If I add 100 to this value I don't see how I could statically prove that no overflow could occur. For that to work, wouldn't I need some way of defining the type of my address as 0 to (2^32-1)-100? If the address is returned from a call to malloc how can I prove that it not only has type addr, but also type addr_100_restricted at compile time?

Peaker 15y ago
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)
- Locke1689 15y ago
  Ah, very clever construction, I like it. Thanks for the input.
  - doublec 15y ago
    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.
- Someone 15y ago
  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 15y ago
    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 15y ago
  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 15y ago
    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.

Peaker 15y ago

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)

Locke1689 15y ago
Ah, very clever construction, I like it. Thanks for the input.
- doublec 15y ago
  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.
Someone 15y ago
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 15y ago
  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 15y ago
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 15y ago
  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.