TheAsprngHacker

As net4all pointed out, your C++ example isn't really dependent types. It's achievable with parametric polymorphism a la System F, AKA the ML-style or Java-style generics.

C++ does have value arguments for templates, however. Perhaps a better example would have been std::array, which takes a size as an argument.

However, C++ still doesn't really have dependent types the same way Agda or Idris has them. One big difference is that C++ templates are only checked upon instantiation. So, this code:

    template<typename T, T a> std::array<int, a + 1> add()
    {
        return {1, 2};
    }

compiles, but when I try to do

    add<int, 0>()

the compiler complains. Because the dependent function type means "forall," it's important that the compiler make sure that it truly does work for all inputs.

I am a highschooler who is interested higher-level theoretical computer science and math. I am motivated to get into a good college because I want to have good educational foundations and the opportunity to meet professors involved in the research areas that I am interested in.

Seeing the college admissions bribery scandal outraged me. Society pressures people my age into getting into a good college as an indicator of worth. Before the controversy, I had already felt cynical about the whole culture of test prep and ungenuine ECs. I feel as though society pressures other teenagers and me into not being true to ourselves, and living our own lives, but instead doing things just for the grades or the attractiveness to college admissions officers. When the bribery became known, it bolstered my belief that elite colleges are places of classism, dishonesty, and phoniness. The girl mentioned in the article who said that she was going to party instead of study is especially a slap in the face for me.

Therefore, I have a conflicting view of elite colleges. On one hand, I greatly admire the professors who work at the colleges, and respect the colleges as places of research. On the other hand, I have a cynical view that elite colleges are a place for social prestige. I had wondered if there was a conflict between the interests of the professors, who would like passionate students, and the interests of the admissions officers, who, according to the scandal, maintain a class barrier by taking bribes instead of admitting students egalitarianly.

This article solidified my thoughts that there is a conflict between the interests of professors and admissions officers.

a-saleh mentioned that Idris and Agda have "stronger type systems." I would like to expand that Idris and Agda (and Coq/Gallina, too) are "dependently typed" programming languages, meaning that types and terms can mix. To my understanding, GHC Haskell is on the way to getting dependent types. GHC currently has the TypeInType and DataKinds extensions, which allow type-level programming. However, Haskell will not get a termination checker, so all types are inhabited by divergent terms. So, you can prove anything. Coq, Agda, and Idris have termination checkers, so you can use them to prove things.

Agda has "Cubical mode," which extends it with Cubical Type Theory, a take on Homotopy Type Theory where the Univalence Axiom is not an axiom, but rather has computational meaning.

Maybe I worded that wrong. In OCaml and other strict languages, `let (rec) a = a` doesn't make sense, because `a` doesn't have a value when you are defining it to be itself. When I write `let a = a` in Haskell, what happens is that `a` is set to a thunk whose code pointer points to its own evaluation code. When the thunk gets forced, it tries to evaluate itself.

Doing my research, I was wrong about the "nonterminating computation" part; when the thunk gets forced, it gets marked as a "black hole," detecting the infinite recursion in this case.

The chapter raises the question of the semantics of

    {
      var a = "outer";
      {
        var a = a;
      }
    }

and

    {
      var a = a;
    }

. Some programming languages have the idea of "let rec" versus "nonrecursive let." In Haskell, `let` is recursive, and because Haskell is lazy, `let a = a` is a nonterminating computation. In OCaml, `let` is non-recursive and `let rec` is recursive, and only certain recursive definitions are allowed. (You can do `let rec a = 0::a`, but not `let rec a = a`.)

Scheme has `let`, where none of the variables are in scope for any definition, `let*`, where each variable is in scope in the successive definitions, and `letrec`, where all of the variable are in scope for all definitions. According to http://www.r6rs.org/final/r6rs.pdf, Scheme initializes letrec'd variables to a "black hole."

According to the article, "The researchers estimate half a million Windows machines received the malicious backdoor through the ASUS update server." I use an Asus computer, but I use GNU/Linux and almost never boot into Windows. Am I affected by the malware? How can I check?

Thanks for the explanation. Your description superficially reminds me of a Markov chain (https://en.wikipedia.org/wiki/Markov_chain). Is this related or is it totally different?

Huh, in this question, there are a lot of words that get repeated five consecutive times: https://stackroboflow.com/#!/question/13733

Is there a reason why? (I don't know anything about AI.)

I use OCaml and I am also writing my own ML dialect, so I would like to ask, what exact aspects of the OCaml syntax don't you like, and what parts of the Haskell syntax do you like in particular? (For example, do you prefer indentation-based syntax?)

I had no idea that the meet/join operations are used in compiler analysis, and I'm curious to find out more. Where can I find out how meet and join are defined on C values, in the context of GCC?

Huh. According to https://en.cppreference.com/w/cpp/container/vector/operator_..., “no bounds checking is performed.” I find cppreference.com generally trustworthy, but maybe it’s wrong here? Or, maybe “no bounds checking” actually means “no guaranteed bounds checking?”

I have some experience in C++, and I am familiar enough with the standard library to remember that operator[] doesn't check bounds while the at member function does. I would assume that the Firefox C++ programmers know this as well. However, maybe I'm wrong or have too much faith?

Or, maybe, the programmer was aware that operator[] didn't perform bounds checking, but opted to use it for some reason? A good way to dissuade people from making unidiomatic choices is to make them more verbose. IMO calling the at function isn't particularly verbose, but if the member function that didn't check bounds were called something like "at_unchecked," perhaps people would be less inclined to use it.

Also, from the snippet in the blog post, note that you can't tell whether the Firefox code used std::vector, C-style arrays, or some non-STL container type. Projects may use their own container types, but your criticism only applies if the programmers were using the C++ standard library.

Thank you for telling me that I can edit titles. I either forgot or didn't realize (since I can't do that on Reddit), and I didn't realize that if I deleted the submission, I wouldn't be able to resubmit it.

Wait a minute... I don't see this submission on Ask HN (although I do see it under "new"). However, when I was looking for it, I happened to find https://news.ycombinator.com/item?id=19187925. As a matter of fact, my submission DID begin with "Why I," and when it appeared, the "Why" didn't appear. Now I realize that I probably didn't make a typo; HN automatically modified my title.

Does the fact that I'm not seeing this submission under "Ask HN" mean that I got somehow auto-flagged or blocked for trying to resubmit, or should I just wait?

You might want to rename your programming language - when I saw this on the Show HN listing, I thought it was the educational programming language Snap!: https://snap.berkeley.edu / https://github.com/jmoenig/Snap.

There are some people in my school who program, but they aren’t interested in type theory. Nevertheless, I think that I would be closer with them if I could just see them more often in terms of class schedules. I will find time to be with them more often.

Thank you for your advice. In the past, I didn’t care about joining other clubs and only cared about my programming hobby. Now, I think that I should be more well-rounded and pick up other activities, especially ones in which I am more likely to find companions. I will find an interesting club to join.

w.r.t being better than others - I go to a school with a strong academic culture. In absolutely no way do people put each other down, not at all, but I feel like there is an underlying motivation to have good ECs to make oneself attractive to colleges. In particular, you mentioned the debate team, which, at least at my school, seems to me like a highly competitive club that boosts college applications. I feel extremely cynical about the culture of people padding college applications, so I had decided previously to ignore clubs and only pursue my passion of programming to be “true to myself.” However, now I feel a desire to join a club out of genuine pursuit of happiness (as opposed to boosting an application). I hope that I will find a club with a passionate and genuine culture, without competitive people.

Before, my mother had told me that I should have activities outside school that I could show for. Part of it was for colleges, as I would have a hard time competing with others if I didn’t do much outside school. However, my mother also said that part of it was being a fuller person. I used to feel frustrated because I felt like she wanted me to do stuff just for college, a motivation that I felt was “phony,” but now I see what she meant about being more active in general.

Thank you for your advice. I really appreciate it. I remember showing a friend in my AP CS class the benefits of sum types for representing errors. (We use Java and I wanted to show a better alternative to its nulls and exceptions). He understood what I showed him and thought it was neat. I think that ties in with what you said about showing “the other person that there is something admirable, in morals and values or skills.” Most people probably don’t care about type theory because they’ve never heard of it, but I hope that if I show it to, say, someone else who is learning programming, they will see the same beauty in it that I do. I think that I will spend more time with this person to become closer friends with him.

I wanted to make this submission longer to better convey how I feel, but I had to cut it down to 2000 characters (including the title apparently). Therefore, it may come across as terse and abrupt.

I personally think that sum types (discriminated unions) are essential for a "modern statically-typed language."

Other people recommended Scratch, but I personally think that it's a poor educational programming language. It's extremely limiting and lacks abstractions such as script-local variables, procedures that return values, and a first-class way to group data. As a result, people pick up poor programming practices such as storing results in global variables or using strings for compound data.

Snap! (https://snap.berkeley.edu/) is based on Scratch and Scheme and features local variables, lambda expressions, and first-class lists (both Scratch array style and Lisp linked-list style). You could also look into Racket (https://racket-lang.org/), another language similar to Scheme. Both these languages have multimedia capabilities that make them attractive to new programmers and a more sensible design that better captures the essence of abstraction and composition.

Andrej Bauer, one of the authors of PL Zoo, also implemented a mini dependently typed language: https://github.com/andrejbauer/spartan-type-theory

Programming languages that support pattern matching support decision tables. This is an OCaml port of the FizzBuzz example (fixing a mistake where the result of the modulo is compared with T and F):

    match n mod 3 = 0, n mod 5 = 0 with
    | true, true -> "FizzBuzz"
    | true, false -> "Fizz"
    | false, true -> "Buzz"
    | false, false -> string_of_int n

This a "cleaner" version that takes advantage of wildcards (which appear in the article, but not in the FizzBuzz):

    match n mod 3, n mod 5 with
    | 0, 0 -> "FizzBuzz"
    | 0, _ -> "Fizz"
    | _, 0 -> "Buzz"
    | _, _ -> string_of_int n

Note that the article states, "two rows can’t overlap in what inputs they cover," but in case analyses expressions of PLs with pattern matching, two rows can share a non-empty set of common matches and the higher row will take precedence.

I don't know the credibility of this Reddit post, but it might be of interest: https://www.reddit.com/r/learnprogramming/comments/91bjlr/sc...

To my knowledge, Reason is just an alternate syntax over OCaml and the two can be converted to each other. Thus, Reason should have the same semantics as OCaml. As OCaml isn’t just targeted at JavaScript, IMO adding async/await sugar for Reason wouldn’t make sense. (I assume that you mean syntax that desugars to JS promises. Correct me if I misunderstood.)

Although, it would be pretty cool if OCaml got some kind of do-notation (like Haskell), a generalization of async/await sugar for any monad structure...

Software Foundations: https://softwarefoundations.cis.upenn.edu

For information about GHC's internals, I recommend reading https://ghc.haskell.org/trac/ghc. The RTS documentation is at https://ghc.haskell.org/trac/ghc/wiki/Commentary/Rts.

That's a pain point for me as well; what I did was edit the URL to make the anchor fragment #(n) where n is the index of the desired slide.

First, you should know that C++11, the C++ standard ratified in 2011, redesigns the language to promote safer and more expressive code. C++11 introduces rvalue references, std::unique_ptr (a smart pointer with unique ownership semantics and a move constructor, superseding std::auto_ptr), auto (type inference), and container iteration syntactic sugar. C++14 and C++17 enhance the changes brought by C++11.

Know about RAII, ownership, move semantics, and smart pointers. Please know that some common C idioms are considered poor C++. (E.g. resource cleanup via goto is superseded by destructors, and malloc and free are superseded by new and delete, which in turn are discouraged in favor of smart pointer RAII.)

Modern C++ is a good programming language, but unfortunately, many resources don’t teach it. Make sure that the resource covers C++11 at earliest. Bjarne Stroustrup, the original implementor of C++, has written some good books. Herb Sutter is another notable C++ author. See also https://stackoverflow.com/q/388242/8887578.

Really? If OCaml has a compiler to Wasm, I’m not aware of it. I’m only aware that it compiles to JS (via js_of_ocaml or Bucklescript). Could I please have a link to the Wasm compiler if you have it?

I read somewhere that an OCaml to LLVM compiler was attempted, but people had problems with the GC aspect. I don’t know if this claim is true, though.