Live data from Hacker News

OCaml Programming: Correct and Efficient and Beautiful

cs3110.github.io

31–40 of 60 posts

Re: OCaml Programming: Correct and Efficient and Beautiful

#31

I just want OCAML to have curly braces, please. And the variable scope thing in OCAML is extremely off putting.

You can use the ReasonML syntax with the standard OCaml toolchain, it's the same language with curly braces. (Not to be confused with ReScript which spun off of it, but is now a different language that only targets the JavaScript stack.)

Do you simply dislike the OCaml syntax or is it some particular quirk?

> the variable scope thing

The what thing? Variables are just lexically scoped, are you referring to shadowing?

Re: OCaml Programming: Correct and Efficient and Beautiful

#32

Earlier quoted context omitted.

I started with SML in the 1980's, implementing a core math algorithm (Grobner bases) used in my K&R C computer algebra system Macaulay. Then I got this idea there should be a related algorithm in a different problem domain (Hilbert bases) and I managed to convert my code in twenty minutes. It ran. This completely blew my mind, on par with switching from punched card Fortran to an APL terminal in the 1970's. Everyone…

Have you looked at Idris 2? I'm 53, impressed that you're still going at it at 69!

Yes. I'm impressed with Idris 2. I love how it uses Chez Scheme, my favorite scheme implementation. I contributed for a bit to getting Idris installation working on Apple Silicon Macs based on Racket's port of Chez Scheme, only to learn that I was working with Idris instructions that hadn't been updated.

Lean 4 is a better supported effort, with traction among mathematicians because of the math formalization goal.

I have more reasons to want to learn Lean 4. Peel away their syntax, and Lean 4 proofs are the word problem for typed trees with recursion. I find the reliance of AI on artificial neurons as arbitrary as so many advanced life forms on Earth sharing the same paltry code base for eyes, a nose, a mouth, and GI tracts. Just as many physicists see life as inevitable, in a billion runs of our simulation I'm sure AI would arise based on many foundations. Our AI fakes recursion effectively using many layers, but staring at the elementary particles that make up Lean proofs one sees a reification of thought itself, with recursion a native feature. I have to believe this would make a stronger foundation for AI.

I don't get that same rush looking at Idris. Using Lean 4 for general purpose programming? It must be good training.

Re: OCaml Programming: Correct and Efficient and Beautiful

#34

I would take the FP zealots more seriously if they stopped asserting that FP makes things more correct. Zero evidence that this is the case. I can tell you that debugging a compiler written in ML is a dumpster fire compared to debugging a compiler written in C++. If take C++ over any FP language for compilers any day of the week.

OCaml is not just FP. It's FP + strong static typing + modular programming + exhaustive pattern matching + fast compiles + great set of built-in compiler lints (eg unused code warnings, mutation warnings). All of these things together help write very reliable code.

Re: OCaml Programming: Correct and Efficient and Beautiful

#35

Earlier quoted context omitted.

Have you looked at Idris 2? I'm 53, impressed that you're still going at it at 69!

Yes. I'm impressed with Idris 2. I love how it uses Chez Scheme, my favorite scheme implementation. I contributed for a bit to getting Idris installation working on Apple Silicon Macs based on Racket's port of Chez Scheme, only to learn that I was working with Idris instructions that hadn't been updated. Lean 4 is a better supported effort, with traction among mathematicians because of the math formalization goal. I…

I'll have to have a look at Lean 4 then.

The simulation hypothesis has a flaw IMHO- If it is modelable and therefore computable, it may be subject to the halting problem

Re: OCaml Programming: Correct and Efficient and Beautiful

#36

I would take the FP zealots more seriously if they stopped asserting that FP makes things more correct. Zero evidence that this is the case. I can tell you that debugging a compiler written in ML is a dumpster fire compared to debugging a compiler written in C++. If take C++ over any FP language for compilers any day of the week.

OCaml is not just FP. It's FP + strong static typing + modular programming + exhaustive pattern matching + fast compiles + great set of built-in compiler lints (eg unused code warnings, mutation warnings). All of these things together help write very reliable code.

There is no evidence that any of those things lead to more correctness.

It’s all feels

Re: OCaml Programming: Correct and Efficient and Beautiful

#37

I would take the FP zealots more seriously if they stopped asserting that FP makes things more correct. Zero evidence that this is the case. I can tell you that debugging a compiler written in ML is a dumpster fire compared to debugging a compiler written in C++. If take C++ over any FP language for compilers any day of the week.

Yet all mainstream languages, including C++, keep adding FP concepts.

Better spend some time having fun with std::variant, visit, and ranges transformers.

Re: OCaml Programming: Correct and Efficient and Beautiful

#38

Earlier quoted context omitted.

OCaml is not just FP. It's FP + strong static typing + modular programming + exhaustive pattern matching + fast compiles + great set of built-in compiler lints (eg unused code warnings, mutation warnings). All of these things together help write very reliable code.

There is no evidence that any of those things lead to more correctness. It’s all feels

There's plenty of evidence. Here's the OCaml compiler catching a redundant rule in the Unicode line-breaking algorithm: https://www.unicode.org/mail-arch/unicode-ml/y2020-m03/0000....

People who like rejecting this kind of stuff as 'feels' are ironically also being guided by their 'feels'.

Re: OCaml Programming: Correct and Efficient and Beautiful

#39
post #25
post #4

Could an OCaml expert give a quick take on the view that if FP, why not go all the way and do Haskell instead? I mean, if "correct, efficient, beautiful" are attributes of OCaml (and I know opinions differ, but let's assume for a moment..) then shouldn't they be attributes of Haskell too, maybe even more so in some ways?

My take is that OCaml lets you sneak a little mutation in, with a little effort, which can make a huge difference in the performance of some algorithms.

Yeah. I agree, I have shaved of a few seconds on my algorithm computation through mutation. I felt like I cheated though.

Re: OCaml Programming: Correct and Efficient and Beautiful

#40

I would take the FP zealots more seriously if they stopped asserting that FP makes things more correct. Zero evidence that this is the case. I can tell you that debugging a compiler written in ML is a dumpster fire compared to debugging a compiler written in C++. If take C++ over any FP language for compilers any day of the week.

> I would take the FP zealots more seriously if they stopped asserting that FP makes things more correct.

Depends on the correctness requirements in question. But overall you are 100% correct about this.

FP, among other aspects, enables and promotes some ways of reasoning, for instance when mutation is avoided, that can be relatively easy to use to verify correctness of certain types of properties. For instance, induction proofs and some other kinds of mathematical proofs. However, for some other types of correctness properties, imperative programming can be easier to reason about than FP. One possible example is in regards to implementation of algorithms, where for instance an implementation of quicksort in C is likely to be more concise and clearer than a "true" quicksort implementation in Haskell. Another possible example is (if one assumes that FP requires garbage collection) that of hard real-time systems, for instance some types of medical devices, where even though some types of garbage collection may be viable, approaches like forgoing dynamic memory allocation (no malloc, no reference counting, no types of garbage collection, etc.) may be easier to reason about regarding achieving the correctness requirement of hard real-time.

Overall, I definitely agree that ML and FP are not the best for achieving correctness in all cases.

I personally like to pick and choose between FP and other approaches, and mix them in different ways dependent on the project or task at hand. Like, a purely functional interface with internal mutation in the implementation for optimization. Or, some mutable API that uses FP for some aspects of the implementation where FP is easier to reason about.

> I can tell you that debugging a compiler written in ML is a dumpster fire compared to debugging a compiler written in C++. If take C++ over any FP language for compilers any day of the week.

For larger compilers for some requirements, I could for some projects imagine that this is true. But, for smaller compilers with relatively few requirements, the pattern matching and tagged union features of modern ML languages are very popular, and I like having access to those features when writing smaller compilers. If you do not mind spending the time to expound on this topic, I would very much like to know more. Or, maybe some links, like blog posts, that discuss this topic. I am genuinely curious. A blog post could also be shared elsewhere, instead of just lost in some Hacker News discussion. (Maybe I should start blogging myself).

Also, Hacker News/Ycombinator is censorship-infested.

Post reply on HN