3 ms·

ETA: I was missing something - thanks! I may well be missing something, but IIUC the linearity in Haskell is on the arrows - the function promises to use that

ETA: I was missing something - thanks! I may well be missing something, but IIUC the linearity in Haskell is on the arrows - the function promises to use that argument exactly once (if it terminates - and never more than once). I think this means `splitDArray` is broken. It consumes the linear argument, but then gives us two DArrays that we can forget to fill (or, probably not as bad, fill multiple times). If that's the case, we probably want something more like splitDArray :: Int -> DArray #-> (DArray #-> DArray #-> a) -> a Please someone correct me if I've missed something :)

danidiaz 6y ago
The only way to get hold of a DArray is inside the callback of the "alloc" function: alloc :: Int -> (DArray a ⊸ ()) ⊸ Array a According to the linear Haskell paper: "f :: s ⊸ t guarantees that if (f u) is consumed exactly once, then the argument u is consumed exactly once." Also: "To consume a pair exactly once, pattern-match on it, and consume each component exactly once" So, if we call splitDArray inside that callback, then we are obliged to consume each of the resulting (DArray a, DArray a) exactly once to satisfy the constraint that the input is consumed exactly once.
- dllthomas 6y ago
  Ah, right. My new understanding, still somewhat shaky (partly because I don't have a recent enough version of GHC to play with these): Something passed into a function as a linear argument is considered to be "used" as many times as the result is consumed. So if we try to use either resulting `DArray` more than once (or forget to use one of them) we will have used the original `DArray` more than once (or forgotten to use it, ... or both). As you point out, that can't be done because we're inside the callback (although I'd followed that bit originally). And that's why we have `Unrestricted` - for returning results we can reuse (or needn't use) while still consuming the arguments exactly once.

danidiaz 6y ago

The only way to get hold of a DArray is inside the callback of the "alloc" function: alloc :: Int -> (DArray a ⊸ ()) ⊸ Array a According to the linear Haskell paper: "f :: s ⊸ t guarantees that if (f u) is consumed exactly once, then the argument u is consumed exactly once." Also: "To consume a pair exactly once, pattern-match on it, and consume each component exactly once" So, if we call splitDArray inside that callback, then we are obliged to consume each of the resulting (DArray a, DArray a) exactly once to satisfy the constraint that the input is consumed exactly once.

dllthomas 6y ago
Ah, right. My new understanding, still somewhat shaky (partly because I don't have a recent enough version of GHC to play with these): Something passed into a function as a linear argument is considered to be "used" as many times as the result is consumed. So if we try to use either resulting `DArray` more than once (or forget to use one of them) we will have used the original `DArray` more than once (or forgotten to use it, ... or both). As you point out, that can't be done because we're inside the callback (although I'd followed that bit originally). And that's why we have `Unrestricted` - for returning results we can reuse (or needn't use) while still consuming the arguments exactly once.