4 ms·

Funny that until yesterday, I had never even heard the name Idris, and now I find it mentioned in two HN articles within 24 hours. Will definitely check it out

Funny that until yesterday, I had never even heard the name Idris, and now I find it mentioned in two HN articles within 24 hours. Will definitely check it out as I’m fond of types. But I also like to imagine Big Typecheck trying to manipulate HN readers into abandoning untyped languages.

the_only_law 5y ago
> Funny that until yesterday, I had never even heard the name Idris, and now I find it mentioned in two HN articles within 24 hours. there's some sort of phenomenon for this, but I can’t recall the name atm.
- c2xlZXB5Cg 5y ago
  Baader–Meinhof phenomenon or Frequency illusion It happens to me when I want to buy a specific car. I see it everywhere.
  - lanna 5y ago
    It happens to me with the Baader–Meinhof phenomenon every time I hear about the Baader–Meinhof phenomenon
- deleted 5y ago
  [deleted]
turbinerneiter 5y ago
Here is my view on this. In the beginning types were useless and hard. Then we made typeless languages so we didn't need to bother with useless and hard types. Then we figured out how to make types easier and useful. 1. C - types represent memory layout, which the programmer doesn't care about, are not useful for error handling and control flow and you have to type them out and remember which one is which. 2. Python - Yolo, nothing matters, everything goes. eZ. Shit, why does this code break after refactoring? 3. Rust - Types are inferred, IDEs and the compiler basically tell you what to do and the types are safeguards, rails and handle logic. Best thing: most of this stuff goes back to the olde languages as well. I.e. IDEs make types in C easier, type hints in Python help with refactoring and so on. So I think w won't even need to manipulate people out if untyped languages. The academic research that helps make programming better will reach all popular languages. (Please don't every example to verbatim - it's just a rough outline of an idea not meant to be an in depth analysis. Of course types in C weren't usesless, Rust want the first to introduce all if these ideas, ...).
- throwaway894345 5y ago
  I don’t think types were hard originally, but rather the popular typed languages for a very long time were C, C++, and Java and they were loaded with foot guns, or at least the popular advice encouraged you to use those languages in a very difficult to maintain way (e.g., shoehorning inheritance into every problem in C++ and Java) or else they were ergonomic problems (lack of type inference or good tooling). The dynamic languages didn’t share these foot guns, so people wrongly assumed they were type system problems.
  - turbinerneiter 5y ago
    That's a very good observation and I agree!
- laumars 5y ago
  In the beginning, memory layout mattered a lot because computers were limited. Then hardware got better, computers became more accessible and the barrier for programming got lower. Now we have numerous domains of software development covered by numerous different programming languages. The choice is good but because we get drilled that computers are a science people will often squabble that their theory is the one true unified theory.

the_only_law 5y ago

> Funny that until yesterday, I had never even heard the name Idris, and now I find it mentioned in two HN articles within 24 hours. there's some sort of phenomenon for this, but I can’t recall the name atm.

c2xlZXB5Cg 5y ago
Baader–Meinhof phenomenon or Frequency illusion It happens to me when I want to buy a specific car. I see it everywhere.
- lanna 5y ago
  It happens to me with the Baader–Meinhof phenomenon every time I hear about the Baader–Meinhof phenomenon
deleted 5y ago
[deleted]

turbinerneiter 5y ago

Here is my view on this. In the beginning types were useless and hard. Then we made typeless languages so we didn't need to bother with useless and hard types. Then we figured out how to make types easier and useful. 1. C - types represent memory layout, which the programmer doesn't care about, are not useful for error handling and control flow and you have to type them out and remember which one is which. 2. Python - Yolo, nothing matters, everything goes. eZ. Shit, why does this code break after refactoring? 3. Rust - Types are inferred, IDEs and the compiler basically tell you what to do and the types are safeguards, rails and handle logic. Best thing: most of this stuff goes back to the olde languages as well. I.e. IDEs make types in C easier, type hints in Python help with refactoring and so on. So I think w won't even need to manipulate people out if untyped languages. The academic research that helps make programming better will reach all popular languages. (Please don't every example to verbatim - it's just a rough outline of an idea not meant to be an in depth analysis. Of course types in C weren't usesless, Rust want the first to introduce all if these ideas, ...).

throwaway894345 5y ago
I don’t think types were hard originally, but rather the popular typed languages for a very long time were C, C++, and Java and they were loaded with foot guns, or at least the popular advice encouraged you to use those languages in a very difficult to maintain way (e.g., shoehorning inheritance into every problem in C++ and Java) or else they were ergonomic problems (lack of type inference or good tooling). The dynamic languages didn’t share these foot guns, so people wrongly assumed they were type system problems.
- turbinerneiter 5y ago
  That's a very good observation and I agree!
laumars 5y ago
In the beginning, memory layout mattered a lot because computers were limited. Then hardware got better, computers became more accessible and the barrier for programming got lower. Now we have numerous domains of software development covered by numerous different programming languages. The choice is good but because we get drilled that computers are a science people will often squabble that their theory is the one true unified theory.