harpocrates

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.

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.