harpocrates

5 yıl öncediscuss

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

harpocrates

6 yıl öncediscuss

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.

harpocrates

7 yıl öncediscuss

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

harpocrates

7 yıl öncediscuss

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.

harpocrates

7 yıl öncediscuss

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.

harpocrates

8 yıl öncediscuss

> 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

harpocrates

8 yıl öncediscuss

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

harpocrates

8 yıl öncediscuss

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

harpocrates

8 yıl öncediscuss

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.

harpocrates

8 yıl öncediscuss

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

harpocrates

8 yıl öncediscuss

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!

harpocrates

8 yıl öncediscuss

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.

harpocrates

8 yıl öncediscuss

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.

harpocrates

8 yıl öncediscuss

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

harpocrates

8 yıl öncediscuss

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

harpocrates

8 yıl öncediscuss

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

harpocrates

8 yıl öncediscuss

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?

harpocrates

8 yıl öncediscuss

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.

harpocrates

8 yıl öncediscuss

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

harpocrates

8 yıl öncediscuss

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

harpocrates

Submissions

What Is Categorical Data?

GHC proposal for Linear Types

comments