[HN Gopher] Pure destination-passing style in Linear Haskell
___________________________________________________________________
Pure destination-passing style in Linear Haskell
Author : lelf
Score : 51 points
Date : 2020-11-12 22:03 UTC (1 days ago)
(HTM) web link (www.tweag.io)
(TXT) w3m dump (www.tweag.io)
| whateveracct wrote:
| Lots of low-level fun in Haskell's future :)
| WJW wrote:
| A really underappreciated part of Haskell is innovation in
| things other than the type system. Linear types is one of them,
| but STM and lightweight threading were in Haskell long before
| they became popular in other languages.
| kevincox wrote:
| > C programmers don't appear to have a name for it. So it is
| likely that you have never encountered it.
|
| The common name for this is "out parameters"
| masklinn wrote:
| Out parameter would generally be possibly uninitialised memory
| in which the function will put the output data, rather than
| allocated memory which the function will fill.
|
| Out parameter is literally just a workaround for the lack of
| MRV, the callee still controls the allocation.
|
| For instance `pthread_create` uses an out parameter:
| pthread_t threadId; int err = pthread_create(&threadId,
| NULL, &threadFunc, NULL);
|
| the first parameter is uninitialised memory, it's only _written
| to_ by the function. If C had tuples / MRV you'd say
| (int err, pthread_t threadId) = pthread_create(NULL,
| &threadFunc, NULL);
|
| instead.
|
| But might still use a "destination passing" function, because
| the point of destination-passing is to make the caller control
| the allocation, and allow amortisation. "Destination passing"
| is pretty common in low-ish level Rust APIs for instance, while
| "out" parameters is largely forbidden (you'd need a function
| taking a reference to a MaybeUninit or such nonsense).
| kevincox wrote:
| I've commonly seen it used for both. Really anything that the
| function will write to.
| masklinn wrote:
| > I've commonly seen it used for both
|
| That's a good reason to rename one of them because they're
| completely different semantics and behaviour, and confusing
| one for the other is a direct route to segfault city.
| comex wrote:
| From another perspective, they're both performing the
| same operation on different types. With what you'd call
| "destination passing", like char *buf =
| malloc(128); snprintf(buf, 128, "hello");
|
| the function is accepting a pointer to an uninitialized
| array of char, and initializing the array of char. With
| what you'd call an "out parameter", like
| char *buf; asprintf(&buf, "hello");
|
| the function is accepting a pointer to an uninitialized
| _pointer_ to array of char, and initializing the pointer.
| The caller still controls the allocation of storage for
| the pointer itself.
| nextos wrote:
| A bit off-topic, but I see places like Tweag claim to use Haskell
| in production for lots of things, including domains where I would
| never consider this language a good fit like statistics & machine
| learning.
|
| I'm very familiar with the Lisp family of languages (Scheme,
| Common Lisp, Clojure, Dylan, Julia...) and with some from the ML
| as well (SML and Scala).
|
| Is Haskell worth the effort for a small organization like a
| startup or a research lab? If so, in what domains? If one wants
| to have strict guarantees why not using Agda or Idris instead?
| klodolph wrote:
| My experience with Haskell is less "strict guarantees with
| proofs" and more "changes to state are exposed in the type
| system." I also think that Haskell has a much larger ecosystem
| than Agda or Idris, so if you need libraries you can find them.
| dllthomas wrote:
| 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 wrote:
| 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.
|
| It seems that linear Haskell will resort often to this
| continuation-passing idiom.
| ghayes wrote:
| It's worth comparing this to linear types being a first-class
| feature in Idris 2 [0]. It's a hugely exciting direction for FP
| in general.
|
| [0] https://www.type-driven.org.uk/edwinb/linearity-and-
| erasure-...
___________________________________________________________________
(page generated 2020-11-13 23:01 UTC)