DanWaterworth

It's quite confusing, the del operator means different things in each term. del of p is just the gradient of the pressure, but the convective term is more complicated. This may help [1]. The key part is:

Generally the convective derivative of the field u•∇y, the one that contains the covariant derivative of the field, can be interpreted both as involving the streamline tensor derivative of the field u•(∇y), or as involving the streamline directional derivative of the field (u•∇) y, leading to the same result.

[1] https://en.wikipedia.org/wiki/Material_derivative

The question was, "how's that?". My answer was, it's possible for a small dependently typed language to be simpler than Haskell.

I'd already made the assertion that Idris was less complicated than Haskell.

You're technically correct, but in practice, proving that software does confirm to a formal specification is, empirically, a good way of drastically reducing defects.

It's not about turing completeness. Deducing arbitrary properties of programming written in primitive recursive languages is also undecidable. This is why type inference in dependently typed languages is undecidable.

You don't need to solve the halting problem to write provably correct software (that is, software that conforms to a formal specification). The halting problem (and Rice's theorem) come into play when you are trying to deduce things about arbitrary programs written in turing complete languages.

It's like the difference between being able to express proofs in maths, versus having a method of deciding the validity of arbitrary propositions. We can certainly write programs that we can we can prove things about, but given an arbitrary program, we can't always tell whether it will do the right thing.

> It's generally (or maybe universally) more difficult to "get" dependent typing than plain old ML-family static typing.

That's true, but Haskell has come a long way since a direct comparison like that would make sense.

> I mean, this HN comments page alone has multiple threads where people don't think that the "x > y" proof example even works.

I think this is because people have some preconceived idea about what dependent typing is before they come to dependently typed languages. So, not only are they learning about dependent types, but they are also fighting their preconceived notions. That was certainly the case for me.

It's an interesting facet of the human condition; every time we learn a new tool, we have to be reminded that it's not magic.

Now, having become proficient, I have a better intuition for how to get my complex Idris programs to type check than my complex Haskell ones. Idris is actually simpler, it's not just about line counts.

Haskell's type system has accrued complexity over the years, whereas a small dependently typed language can be implemented very easily [1].

[1] https://www.andres-loeh.de/LambdaPi/

> Haskell has no equivalent of the Idris type above, and Go has no equivalent of either the Idris type or the Haskell type. As a result, Idris can prevent many bugs that Haskell can't, and Haskell can prevent many bugs that Go can't. In both cases, we need additional type system features, which make the language more complex.

Type checking Idris is much simpler than Haskell.

OK, that's impressive.

This is more difficult than you might think. LLVM IR more like a family of closely related, but poorly-specified languages, than a language of its own.

There is an interpreter in the LLVM codebase, but this is essentially only possible because it is part of the codebase and so tracks the rest of the project very closely.

Since the network has already been trained, I can't imagine using WebGL is worthwhile. It would interesting to see, either, drawing samples from the equilibrium distribution or training in the browser.

I'd expect either Rank2Types or RankNTypes to be included in Haskell', you may be thinking of ImpredicativeTypes.

Wow, I did not realize ScopedTypeVariables had been around for so long.

That's not anywhere near a complete list of deprecated extensions and there are others that have been completely removed from the language [1]. It's unfortunate that ScopedTypeVariables hasn't been standardised, but there hasn't been a new standard since 2010, so it's not hugely surprising.

https://ghc.haskell.org/trac/ghc/wiki/LanguagePragmaHistory

I don't think this is a flaw, in fact I think it neatly solves the problem of how to extend the language without committing to a design too eagerly and provides a platform for experimentation.

There are pragmas that GHC implements that are now widely held to be problematic, but we wouldn't know this without an implementation, and using pragmas, we are realistically able to deprecate and remove these extensions.

If you'd like strictness by default, there's a pragma for that https://ghc.haskell.org/trac/ghc/wiki/StrictPragma

One way around this is to have typeclasses for all the different kinds of effects you'd like with instances for IO. Then for testing you can use a different instance that produces a value of a free monad.

When will the machines learn...

Same way git does?

Same here, though in my case it was on my list of things to continue building.

You don't need a PhD to use dependent types. I don't have a Bachelor's.

> For instance I have yet to see an easy and simple to use (and as such maintainable) functional widget and gui library.

Like react?

It doesn't need to be finished to be useful.

Same author: http://dev.stephendiehl.com/fun/

You have no reason to. We're talking about a hypothetical future where PyPy has become the reference implementation.

If you are happy using CPython, you can't be terribly concerned with performance. The point is, pypy will run on more platforms than its JIT targets.

I mentioned it because I didn't see it in my scanning of the issue you linked to.

Edit: I should have looked more closely, sorry.

With the literate style, code is prefixed and comments are raw. So, instead of:

    -- foo is a function
    foo :: String -> String

It's

    foo is a function
    > foo :: String -> String

I'm in no way connected to the project. Perhaps you should file an issue.

I think people interested in compilers are disproportionately Haskell inclined.

Here you go. It didn't like my stdio.h. Apparently enums and unions aren't supported, but:

    extern int printf(char *, ...);

    int main(int argc, char argv[]) {
        printf("Hello, world!\n");
        return 0;
    }

Was turned into:

    extern {
        fn printf(arg1 : *mut u8, ...) -> i32;
    }
    #[no_mangle]
    pub unsafe fn main(mut argc : i32, mut argv : *mut u8) -> i32 {
        printf(b"Hello, world!\n\0".as_ptr() as (*mut u8));
        0i32
    }

edit: Also worth noting, it removes all comments. I believe this to be a limitation of language-c [1]

[1] https://hackage.haskell.org/package/language-c