Pure destination-passing style in Linear Haskell | Hacker News Reader

Pure destination-passing style in Linear Haskell

tweag.io

89 pointslelf23 comments

> 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"

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).

I've commonly seen it used for both. Really anything that the function will write to.

> 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.

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.

At this point of the lifetime C-language, hoping for the commonly accepted terminology to change, is probably futile. Anyway, for out parameters, the common convention is:

Caller provides one object for output:

   void callee(Obj *obj);

Caller provides an array for output:

    void callee(Obj *obj, size_t obj_size);

Caller provides an pointer, to which callee allocates a new object:

    void callee(Obj **obj)

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-...

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 :)

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.

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 family as well (SML and Scala).

Is Haskell worth the effort for a small organization like a startup or a research lab? Would it bring something different when compared to those other languages? If so, in what domains? If one wants to have strict guarantees in the form of proofs why not using Agda or Idris instead?

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.

Haskell has a better and more mature runtime as well.

Of all the languages I've used in production on the backend (Haskell, JVM, Go, Python), GHC's RTS is definitely the best.

>If one wants to have strict guarantees in the form of proofs why not using Agda or Idris instead?

Because they're research languages. The amount of non-toy software actually verified in them is zero. I'm not even sure if there's any non-toy software written in Idris besides the Idris compiler itself.

Coq's track record is better, but its language is ugly as hell in comparison (and to actually do anything you'd need to extract to Ocaml/Haskell anyway and the same applies to Agda).

Probably not, but it is fun and enjoyable to use for curious, creative and intellectual developers.

* The type-system is a delightful and lets you control and secure your program in a unique way.

* The language model and idioms are elegant and highly expressive.

* Once you become proficient you can write code as fast as you would with python (without libraries/frameworks)

On top of this the library ecosystem, and development tools are about on par with general standards, and the compiler + runtime are exceptional.

As of writing HN says my post [1] was made 2 days ago and this was post was made 15 hours ago. Not sure why it wasn't duped.

[1] https://news.ycombinator.com/item?id=25068394

> Are reposts ok?

> If a story has not had significant attention in the last year or so, a small number of reposts is ok. Otherwise we bury reposts as duplicates. (https://news.ycombinator.com/newsfaq.html)

1 upvote and 0 comments clearly isn't "significant attention", so why would it be?

I didn't mean explicit reposts. I thought if the same link was submitted within a short time frame a new submission would not be created, but rather the submitter would be automatically re-directed older post (and possibly automatically upvote it). It's been a while since I've experienced this as I always do a search before submitting these days.

Lots of low-level fun in Haskell's future :)

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.

That is technically correct, but green threads were available in Java 1.1 :). They just weren't popular enough (I guess).

I actually think green threads in GHC narrowly beat out green threads in Java (I think GHC got them in 1996 or earlier). But I also don't think Haskell was the first language to get them.

Haskell's been around for a long time! GHC was begun in 1989.

Quite common in ATS.

Reply on news.ycombinator.com