harpocrates

GHC also uses Demarau-Levenshtein [0]. The fuzzy lookup function gets re-used for a couple places too (including whatever you encountered in GHCi).

[0]: https://github.com/ghc/ghc/blob/25977ab542a30df4ae71d9699d01...

For anyone curious about the difference between the two: Hughes' pretty printer works really well for pretty-printing Haskell code, but Wadler's is more flexible for pretty-printing C-style languages where there is a dedented closing brace at the end of scopes.

It is 100% true that Hughes' paper is a better introduction to the idea of having algebraic document combinators. One can skim Hughes' and then feel at ease using a library that implements Wadler's printer - the bigger differences between the two libraries are tucked away in the layout algorithms and the APIs are similar.

As I've already posted elsewhere on this thread, such a tool has been developed in parallel (and with the intent to consume the output of) c2rust. Development on that occurs here: https://github.com/immunant/c2rust/tree/master/c2rust-refact....

Step 2 has been happening concurrently, and pretty much since the start of the project. See https://github.com/immunant/c2rust/tree/master/c2rust-refact.... It is just a lot tougher to get right, so it gets less publicity.

Safety in the form of tightly-fitting types is great, but the signatures definitely suffer a bit in readability (otherwise, Haskell signatures are generally quite helpful when deciphering a functions purpose). I understand why it needs to be this way, but this signature is nasty looking:

    makePCATypeSafe
      :: forall d x y. (AllConstrained SingI '[d,x,y], d <= x ~ 'True)
      => Proxy (d :: Nat) -> DimMatrix D y x Double -> TypeSafePCA

In (pseudo code), dependent types would really help out a lot:

    makePCATypeSafe
      :: forall (d :: Natural) (x :: Natural) (y :: Natural). d <= x
      => Proxy d -> DimMatrix D y x Double -> TypeSafePCA

It sometimes feels like GHC is a kitchen sink for type-level extensions. I wish the bar for entry for new extensions of this sort was higher and the language a bit more cohesive.

> It's available in Haskell as a first class citizen.

Not really. Haskell's laziness makes it easier to write functions that are memoized, but it does not automagically memoize functions. And how could it without incurring a non-trivial runtime space/time cost?

Haskell's purity is what makes it easier to write libraries that facilitate building memoized versions of functions in a transparent way (and that are obviously correct). For instance, I usually reach for [data-memocombinators][0], which happens to have a fibonacci example at the top of the docs:

    import qualified Data.MemoCombinators as Memo

    fib = Memo.integral fib'
       where
       fib' 0 = 0
       fib' 1 = 1
       fib' x = fib (x-1) + fib (x-2)

  [0]: http://hackage.haskell.org/package/data-memocombinators-0.5.1/docs/Data-MemoCombinators.html

`@implicitNotFound` still only gives you a top-level failure message. Also, my comment was aimed more at developers of libraries with complex implicit derivations not the consumers of such libraries.

I heartily recommend [splain][0] to anyone debugging non-trivial implicits. It is a scalac compiler plugin that, among other things, will swap out the horribly unhelpful "implicit not found" or "diverging implicit expansion" messages for an indented and annotated representation of the search tree that the compiler went through before giving up.

`-Xlog-implicits` is good to use every now and then, but it quickly becomes unreadable for any decent sized project.

  [0]: https://github.com/tek/splain

FWIW we've spent a lot of time trying to re-engineer the control-flow translation to be heuristic-friendly in c2rust. We've extended and tweaked the Relooper algorithm in hopes of preserving more of the initial control flow. It still isn't great, but it is getting better.

Offhand, here are some sizeable additions:

* Keep track of some extra information from the C source about what basic blocks were in loops or branch points, then use than information to try to extract back out similar looking Rust

* Support translating `switch` to `match`, complete with collapsing some patterns together

* Properly handle initialization

That said, c2rust can be invoked _without_ relooper enabled if you so wish. In that case, it will simply refuse to translate code with goto's.

The idea is that this is a first step towards safe Rust. First, you convert to unsafe (but semantically preserving) Rust, then you refactor. The refactor stage probably will involve changing some semantics (read: fixing bugs), or perhaps proving some properties with an SMT solver before applying certain transformations (converting a `libc::c_int` to an `i32`, or a `*const i32` to a `&i32`).

I'm a primary contributor to c2rust and I may be the person "stolen" away from corrode. I'd like to apologize if it feels like we ripped off ideas without giving due credit - the project wasn't really supposed to "discovered" so soon. The website was a throwaway idea, a means of easily sharing our work in a limited circle while avoiding both the DARPA approval and the sub-par build process (you have to build a huge chunk of Clang).

So here is me acknowledging Jamey's work: I personally did take inspiration from Corrode, and I was expecting to work on Corrode proper when I joined Galois. I've re-read the CFG module of Corrode several times (as well as the Mozilla paper, and some older literature).

All that said, I also want to point out that Corrode hasn't had any activity at all since last April - and that's not for want of PRs piling up. I'm not criticizing here, since I understand that managing an open source can be quite time-consuming and stressful, but I feel like this also does need to be mentioned. Also, c2rust can be freely forked. Once the DARPA funding runs out, it is my hope that the Rust community will become the maintainers.

Finally, regarding the many improvements that can be automated: that is next up on our plate!

I have very mixed feelings about using parser generators instead of hand written parsers. I've contributed to GHC's parser grammar and spent a lot of time reading Rust's hand-written parser.

On one hand, a grammar is an invaluable tool. It helps keep you honest about ambiguities when you start thinking about adding language features. I think languages should always keep some reference grammar up to date.

That said, I don't think it is a good idea for compilers to use parser generators. A hand-written parser can have better error recovery and more helpful error messages. GHC's parser has some pretty bad parse error message.

Some work was merged into Happy a while ago to support better messages (enabling you to see the expected tokens along with the bad token), but using that in GHC itself is blocked by how complex GHC's tokenizer has become.

Some other applications are more interesting. For instance, finger trees (which back the efficient implementations of a handful of immutable data structures) usually are implemented in a way that requires polymorphic recursion.

The introductory one is known as Baby Rudin and is a pretty good first exposure to real analysis.

I'm not sure I understand: WebAssembly is the output of a (hopefully) optimizing compiler. LLVM is such a compiler backend. If you use WebAssembly today, you are probably going through LLVM.

Perhaps you meant: why not use LLVM IR instead of WebAssembly? If so, allow me to refer you to this comment[1] (from a bit further down in this thread).

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

> No they wouldn't. They still need to turn WebAsm/IR into assembly, which is the thing they already do today anyway. Nothing changes for compilers, other than the potential for optimizations gets much, much worse as the IR is comparatively crippled and restricted to the IR they already have.

Most compilers today have separate assembly generation for MIPS, ARM, x86_64. They could turn source into WebAssembly and no more (the job of WebAssembly -> native is left to some other architecture specific compiler).

> This has never been the result of CPU instructions. That's a library problem, not an IR problem. WebAsm does nothing to help with this, particularly as it intentionally has no real standard library to speak of.

If any one language targets WebAssembly, as long as you resolve your libraries within that language, you'll be able to deploy to any target that supports WebAssembly. This is pretty much the defacto solution to the library problem in a variety of ecosystems: in Java you'll make a fatjar and in C/C++/Rust you'll make a staticly linked binary.

> WebAsm is an intermediate, not a source. Formally verifying it is about as useful as formally verifying assembly. Which is to say, not useful at all. That doesn't help you verify anything about your code, which was a compiler, optimizer, and god knows what else away from the webasm that was generated.

Are you familiar with binary analysis?

What other low-level format supports my points (a), (b), and (c)? And has an actual spec?

EDIT: you've since added some examples. Here are my (very subjective) opinions:

- The JVM isn't really all that low-level - it eeks out a lot of performance at runtime. Plus, you need to have GC, which tends to increase memory requirements and complicate real-time constraints.

- NaCL was interesting but its spec wasn't as good. IIRC Google didn't do too much in the way of asking for public input. I think some folks had some security concerns too. I really like WebAssembly's spec - I don't see any typing judgements or small-step rules for NaCL.

- Wasn't ANDF unix-bound?

One thing that continues to amaze me is that WebAssembly isn't being discussed more outside of the context of the web. Think about it just as a format that (a) is low-level enough to support performance tricks, (b) is fast to turn into native code, and (c) easy to check.

Compilers could stop worrying about obscure/old architectures. Deploying an application onto multiple platforms is no longer a problem. Sandboxing is much simpler. Formal verification becomes possible (the WebAssembly spec actually reads like a spec, unlike the C standard which reads more like a religious text).

I'm so excited about WebAssembly, but really not because of the web.

Yes, when people use them. There is no really elegant way of adding a type annotation to a `do` block.

    (do x <- pure 1
        y <- pure 5
        pure (x + y)) :: Maybe Int

It isn't uncommon to have to scan the `do` block for some statement that constrains the monad somehow.

This is a known and discussed problem, so I'll refer you to the article usually reference around this issue: https://wiki.haskell.org/Do_notation_considered_harmful

You've changed my mind on adding special syntax for `async`, generators, and results (`?`). I previously thought it was a big mistake given that these all generalize as monads (granted, there is some ground to be covered before such an abstraction would fit in Rust).

What I hadn't considered: specialized syntax leads to better error messages for the most common cases. That's probably quite a good thing, especially since descriptive error messages make me much more productive. (Not to mention that specialized syntax also acts as a type annotation of sorts too; a common problem I have in Haskell is figuring out _which_ monad a certain `do` block is using.)

This is not possible in regular Haskell. For one, it isn't obvious how to do such a desugaring and, even if it were, this is pretty gross.

I remember a co-worker finding some weird combination of old extensions which allowed you to do something gross-ish of this form. I've _never_ seen such a thing in real life.

The only practical issue that comes close to this is sometimes trying to figure out _what_ monad a particular `do` block is running with (my mental type inference falls short of the compiler's).

> People underestimate the compiler cost of deriving instances. It adds up very fast if you derive lots of functors and foldables in your quest for unique names everywhere.

Do you pay this price when you derive via a `newtype`? Or does GHC figure out that the instance it would write out would be identical (modulo coercions)?

The comments from the original post[1] of this are still quite relevant. I feel like I've seen this link posted here several times (much more recently than 2009), but I can't find the links.

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

This is a cool (if not particularly new) paper. Interestingly enough, the [vector library][0] mentioned in the paper isn't just a research project - it is one of the most widely used Haskell libraries for vector.

That said, I am saddened by the state of vectorization in GHC. AFAICT it seems all but abandoned [1]. I think there is some hope on this front in the recent progress that has been made on the LLVM backend (producing good input code for LLVM, and choosing the most fruitful LLVM optimization passes) [2].

  [0]: https://hackage.haskell.org/package/vector
  [1]: https://www.reddit.com/r/haskell/comments/51gvxl/whatever_happened_to_automatic_vectorization_in/
  [2]: https://ghc.haskell.org/trac/ghc/wiki/ImprovedLLVMBackend

I think this actually misses the biggest point. Complex numbers are special because they are an algebraic closure of the real numbers (what makes the real numbers interesting should be more obvious), and because Zorn's lemma tells us that such a closure is unique (up to isomorphism). In other words, complex numbers are precisely what you need to add to real numbers in order to always be able to solve polynomial equations.

TL;DR: complex numbers are the unique algebraic extension to the real numbers

> It may even be fair to say that Haskell's typeclasses make it more like an object-oriented programming language.

The trick here is defining "object-oriented". In modern object-oriented languages, I usually assume that involves encapsulation of state inside of boxes called objects. In that sense, type classes are quite different.

Methods on objects generally mutate or provide views into the contents of the box, while methods in type classes are just regular functions. Critically, there is no inner mutation or privileged view into data via type classes.

> They have things like properties and multiple inheritance

How do they have properties? Also, they don't have multiple inheritance - a type can only ever have one instance of any given typeclass.

> Even Wadler has a section leading with "Object-oriented programming."

I read Wadler's paragraph on object-oriented programming (bottom of page 3) more as a highlight of the fundamental _difference_ between type classes and object-oriented classes. The only similarity between typeclasses and classes are that they are the mechanisms by which runtime dispatch is achieved.

Diagnosing oneself with imposter syndrome (or, at the other end of the spectrum, recognizing the Dunning–Kruger effect in oneself) is a perfect catch 22.

This article hits the nail on the head: being slightly paranoid and doubting oneself is a pretty essential part of being a good developer. It's (in most cases) pretty normal. The key is to try and detach your self-worth from the problems you face. You aren't any less good because you couldn't solve that bug last week.

I would hardly identify lazy evaluation as a core feature of functional programming. It definitely forced Haskell not to compromise on purity but, as SPJ himself has pointed out, that may be the only strong thing it has going for it[0]. Currying is also nice, but I'm still not sure that is _core_ to FP.

What Lisp is really missing from an FP perspective is purity. In fact, maybe a pure variant of Lisp would be perfect for teaching.

[0]: https://www.microsoft.com/en-us/research/publication/wearing...

Is this implemented yet? The paper you linked is a draft. I'm glad C++ is doing this.

> Historically, C++ used includes so that it could be compatible with C.

I think it is more the case that C++ slowly splintered off C and never broke free completely of #include. Rust is also quite compatible with C without supporting anything like #include. It even has a module system!

Actually, those are the type errors I _like_ having (and don't always have: Scala will implicitly convert `Int` to `Long`), although I concede this is a matter of opinion. However, I am definitely less impressed by the unhelpful type errors one gets when implicits somehow fail...