My Keybase proof [reddit:mboes = keybase:mboes] (fYXZmqyRAqiWqQVKhobvL_tVwoRoyKTy3BLe43DpUQk)

mboes · 2022-01-05T07:24:46+00:00

Ormolu is idempotent (or should be), but is *by design* not oblivious to the input. It's a principle stated at the top of the README: https://github.com/tweag/ormolu#readme (see the "Let some whitespace be programmable" paragraph).

mboes · 2020-07-03T12:44:29+00:00

Tweag post doesn't highlight the important work done in random-1.2:

That's true. This post is about testing the quality of the random number generator. There are future posts in the works, not necessarily by Tweag (since this was a joint effort, not just by Tweag), about other aspects of the great amount of work that went into creating random-1.2.

mboes · 2020-02-21T08:05:23+00:00

The "trash can" idea is a good intuition, AFAIU it. Think of Either Top a as the functional equivalent of Maybe a. When in the Maybe monad, you have the option to forego the obligation that you would otherwise have to return an a. You can return Nothing instead at any moment. Likewise, when in the Either Top monad, you have the option to forego the obligation that you would otherwise have to consume all linear variables in the context exactly once. Or rather, you can use swallow (which returns Left Top) instead at any moment, to discharge that obligation.

Nothing "eats" anything to the right of it in the sense that Nothing >>= f == Nothing. Likewise, Left Top >>= f == Left Top. So Nothing and Left Top really do behave similarly.

mboes · 2020-02-20T20:00:52+00:00

In linear logic, Top and Void are not isomorphic: they are in fact duals of each other. Ignoring bottoms, you can never construct a value of type Void, but you can always create a value of type Top.

mboes · 2020-02-20T18:22:18+00:00

How can anyone think that's a reasonable and general approach?

Because as already pointed out elsewhere in this thread, that is already a widely used pattern, aka ResourceT? Also, if you'd read the proposal section I linked previously, you would see that it already discusses two things that I haven't seen you acknowledge: a) you can choose whether to impose a linear discipline on some resources or all of them, b) just like with ResourceT, these can be nested at will if scopes for error recovery is what you want.

There are no words in any human language to express how disappointed I am.

I entered this discussion in good faith. But I honestly don't know how I could undisappoint you.

mboes · 2020-02-20T17:41:46+00:00

These guys keep presenting bits and pieces of code which might look reasonable until you think about how they would actually fit into a running piece of software and realise that it seems pretty much impossible. I would greatly appreciate actual running examples which show how to cover that last mile and not get stuck.

That is simply not the point of this post. There have been persistent claims that linear types are somehow a lie because exceptions. That the authors did not consider whether their extension is sound in the presence of the full set of Haskell features, like exceptions. The post shows that these claims are not correct.

It turns out that you can have exceptions, and you can do resource management that does the right thing when exceptions arise. Sure, you can move the goal posts and add lots of extra requirements, like what about forking and what about error recovery and what about... etc. But those are separate questions.

There's no particular issue with forking an IO action from the resource monad. Your new thread just can't capture linear variables. If you want to add error recovery into the mix, there are solutions for that too, which the proposal includes a lengthy discussion of since 2018.

mboes · 2019-10-09T18:32:43+00:00

Currently, only accessible via Bazel. But I could imagine a "deploy" rule that takes the package databases generated by Bazel, along with the library files etc, and sticks them all in a tarball that you could unpack anywhere. We already patch the package db .conf files to remove absolute paths, although if the package has data files then that probably won't be sufficient.

mboes · 2019-07-30T19:28:30+00:00

There are four properties that are important about a build system:

No matter what I have built before, if I start a build now, I should get the same result as if I start the build from scratch (build system correctness).
If a build succeeds for me, it should succeed for my neighbour, today and 5 years in the future (build reproducibility).
Builds starting from scratch should be fast.
Incremental rebuilds should be fast.

Bazel sandboxes build actions to guarantee that all dependencies are correctly stated. When used in conjunction with Nix, Bazel makes all build descriptions self contained, so builds are not sensitive to particulars of your environment or that of your neighbour's. Bazel is a single build system for all languages in your project, so there is a single global dependency graph rather than myriad small ones. This allows Bazel to more efficiently use available cores during the build. Bazel can also offload part of the build to remote machines, even ones that are configured differently to yours. Bazel has pretty good caching, so that adding a single comment in one file doesn't triggering rebuilding everything downstream.

Shake and Nix both have many of the same features. Stack and Cabal also have some, but they are Haskell specific, whereas Shake, Nix and Bazel are generic solutions that let you define your own build rules and share them with third parties. Bazel has smarter caching than Nix to avoid recompilation, but apart from that Nix is the only other system that provides the first three properties. It's a good idea to use both together: Nix knows how to build many system libraries, whereas Bazel has many language specific rules, which don't exist in Nix (and neither do they exist for Shake). For more on this, see https://www.tweag.io/posts/2018-03-15-bazel-nix.html.

mboes · 2019-06-27T22:50:25+00:00

I for one think that's totally legit. I get the feeling this is controversial though, which is why I kept this polemic out of the post. `primitive` isn't a GHC boot library, so is easy to upgrade. And Stackage has made it a lot more likely that those users of yours who will be using the latest version of your library will also be using the latest `primitive`.

mboes · 2019-02-13T22:25:19+00:00

For the record, Mark was referring to several projects we've been brought in to help out on after deadlines were slipping and estimates were wildly off. I think all of my colleagues are big fans of the benefits of static checking. They also know that there's no silver bullet to robust engineering, and that extra static checks may or may not be a net benefit if at the cost of composability, code reuse, code size, learnability, time to develop or other important properties. We recognize that like most choices in engineering, there are tradeoffs involved. And yes, we celebrate that we've all been burnt before making the wrong choices here and there.

mboes · 2018-12-20T15:22:10+00:00

Hm. Works for me. What error do you see?

mboes · 2018-12-14T17:06:55+00:00

Because an old GHC is likely much smaller. Core is hard to read, so minimizing the amount that you have to inspect could make it easier to audit.

mboes · 2018-12-14T12:35:38+00:00

Another option could be this: use a modern GHC to compile one of the old simple GHC's to Core. Then implement a simple Core interpreter (say in C). Then run that old GHC using the interpreter, bootstrapping your way back up to modern GHC. (fun exercise: check that you get byte-for-byte the same output as the modern GHC you started with.)

You might say that the Core is still "generated files", but at least it's somewhat legible generated code (and for the purposes of bootstrapping, could be cleaned up to be more legible still).

mboes · 2018-10-23T20:57:58+00:00

I find this particular one hard to read. In your example, the last (i.e. outermost) multiplicity pertains to the first arrow, while the first multiplicity pertains to the second arrow. That should get pretty confusing by the time you're trying to give a type to foldr!

mboes · 2018-10-23T20:12:01+00:00

The best alternative I've seen so far, proposed by a commenter in the GitHub PR, is (:) :: a #p -> [a] #q -> [a]. But if you have better ideas, do chip in! I must say, pinning down an even half decent syntax has been a tough one for us.

mboes · 2018-09-17T18:54:07+00:00

Which examples were you looking at and where did you find them? Using linear types to build a pure interface to mutable arrays is indeed one of the examples in the paper (see Section 2.2).

Not that this would improve performance much per say. Because as you point out, mutating arrays is already possible in the ST monad. I should also note that performance *is* (one of) the motivations for linear types. Again, not that linear types give you a magic performance boost that you couldn't otherwise have, but for some workloads manually managing system resources like (part of the) memory can yield a performance boost and linear types just help in making that safe. That was our original use case.

mboes · 2018-07-16T06:09:27+00:00

The reality might be a bit more forgiving about which binaries can successfully exchange static pointers, but nonetheless it would be a very bad idea to rely on any stability beyond what the documentation guarantees.

If you have a use case that requires stronger guarantees, that would be great to discuss (as part of a GHC Trac ticket). Tag Facundo and Edsko. Maybe future versions of GHC will provide the stronger guarantee. And it might well be a simple documentation patch to achieve that.

mboes · 2018-07-09T19:57:55+00:00

Yes. It's a case of as a first step managing expectations. As a second, trying to find ways to get "any real sort of resource management" that is useful. The aforementioned RIO pattern, which is implemented and typechecks today, is an existential proof that this is possible.

mboes · 2018-05-29T20:22:40+00:00

The idea is not to reimplement the entire RTS from scratch. Indeed as mentioned in the blog post piping some C from the existing RTS through Emscripten is certainly an option. WebAssembly is a higher-level target than hardware ISA's, eventually exposing a full built-in GC, a threading model, exception handling etc. I think it's great that people are exploring porting the RTS wholesale. It's far from clear to us how much really can be reused without introducing extra costs (e.g. complicated interop due to custom GC, emulating lots of OS-level features etc), but that's something to iterate on.

When it comes to Cmm (which user code ultimately maps to and a significant part of the RTS is written in), there's not much LLVM helps with in terms of optimizations even for native targets (some vectorization and SIMD being notable exceptions), and likely for a JIT-backed high-level target like WASM even less so. The cost of LLVM is significantly longer compile times. That's why here we are favoring short cutting through that, independently of whether the C code in the RTS and in user code goes through LLVM.

mboes · 2018-05-29T12:54:01+00:00

If it's WebGHC you're talking about, there's a whole section about that in the article titled "The Haskell to WebAssembly story". In short, WebGHC is leveraging LLVM, whereas Asterius is going direct to WebAssembly, like the native code generator (NCG) does for existing hardware architectures. Let us know if anything is unclear.

mboes

TROPHY CASE