Comment by danidiaz | Hacker News Reader

Comment by danidiaz | Hacker News Reader

Parent Full thread

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.

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.

Reply on news.ycombinator.com