6 ms·

Propagating NaNs?? Gah, at least exceptions provide a backtrace. What's needed is a dependent type system (like that of ATS or Ada) that allows the range of al

Propagating NaNs?? Gah, at least exceptions provide a backtrace. What's needed is a dependent type system (like that of ATS or Ada) that allows the range of allowable values for an integer to be decalred. A halfway-smart compiler can then statically check (using e.g. abstract interpretation) that the intermediate results of arithmetic performed on such integers does not exceed the system integer size, and that the results do not exceed the declared size of the result variable. (In fact, if the programmer places runtime checks at the right places, such range declarations aren't even necessary as they can be inferred by the compiler.) Such a system would statically guarantee that no overflow will occur. This means no spurious hard-to-track-down NaN results at runtime.

Locke1689 15y ago
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.

Locke1689 15y ago

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.