gnulinux

88 ms·

961.
by gnulinux 6y ago
Ok but I have 3 million lines of Python code, so that doesn't help me. I'm not gonna spend a year or two writing everything in Julia.
962.
by gnulinux 6y ago
Haha no problem, thanks for your input!
963.
by gnulinux 6y ago
Yes you're right it is inductive, I misread your comment as "it compiles" and once again got lazy and didn't check the link. :(
964.
by gnulinux 6y ago
Cool! Yeah I've been lazy as I don't have Haskell setup on my work computer. So, in short it's just coinductive natural number type. I'd say it's very far from useless, I use Conat in Agda pretty often especially if
965.
by gnulinux 6y ago
What makes Laravel so good and why can't we clone to a framework in say Python?
966.
by gnulinux 6y ago
In this case it looks like `T = Maybe T` is isomorphic to a coinductive natural number type, where `suc = just` and `zero = nothing`. You can see an example implementation of it in Agda: https://github.com/agda/agda-std
967.
by gnulinux 6y ago
I had a similar experience with Prozac, albeit less extreme. I was depressed and very anxious about anything and everything. Started Prozac + CBT therapy, it had no side-effects and I was feeling really much better in a matter of weeks.
968.
by gnulinux 6y ago
Yes, I think we agree.
969.
by gnulinux 6y ago
(AINAL) No I don't think you're correct, which is what I (and others) were trying to explain. Which is also why MIT and Harvard (and many other universities) sued ICE. Here, copy paste from another comment: > 19. Plaintiffs hav
970.
by gnulinux 6y ago
I'm American and I have no idea what's going on either. The admin is behaving very erratic and POTUS is always talking about peripheral issues and doesn't address the current crisis (i.e. COVID, 20% unemployment, depression e
971.
by gnulinux 6y ago
Others gave you good answers but also consider this. There are thousands of PhD students who create value for these universities. They not only do research, help research being made, they also teach others. Kicking all these people out of U
972.
by gnulinux 6y ago
Again, can't speak for haskell. In agda you usually have 2 goals creating a function * Proving a property of some other object. In this case you have to write the type first since type is the theorem you want to prove, and implementati
973.
by gnulinux 6y ago
This is true, I should have mentioned it, although my point still applies to HM style type inference as well.
974.
by gnulinux 6y ago
Makes sense, bad errors is also why I don't use type inference in my code.
975.
by gnulinux 6y ago
I've never written Haskell but I'm a Agda programmer (a Haskell dialect with dependent types) and I almost always put all the types and don't rely on type inference. The obvious exception is if something quick like a =
976.
by gnulinux 6y ago
Why is it not realistic? Is it too slow or too unreadable?
977.
by gnulinux 6y ago
HM is pretty easy implement actually. You just need a unification function, the rest is just a laundry list of rules available everywhere, like Wikipedia. Source: I implemented a typed python dialect as a college project that used HM.
978.
by gnulinux 6y ago
What a strange comment. > Brazil's labor laws treat the "workers" as stupid people This has nothing to do with stupidity, intelligence or anything like that. This has to do with leverage . A multi-national giant corporati
979.
by gnulinux 6y ago
I want to write about my opinions on software but I'm nowhere near experienced enough to have good opinions and I don't want my blog posts to get attached to my professional persona.
980.
by gnulinux 6y ago
"Business logic" is just another name of "logic". E.g. something like "if X is even, then print 'fizz' otherwise print 'fuzz'" is considered business logic.
981.
by gnulinux 6y ago
If they produce competitive CPU on RISC-V that'd be very interesting. I'd like to see a competition between ARM and RISC-V chips, so that ARM is not the monopoly in that niche market (high-end non-x86 chips). I think it's ver
982.
by gnulinux 6y ago
Haskell used to be compiled to C. (not sure if they still use this backend, I think main GHC backend compiles to LLVM). "Doesn't have garbage collector" is not a good reason not to be able to compile to C, surely garbage coll
983.
by gnulinux 6y ago
> I was a pro-education person I must say: I'm genuinely surprised reading this sentence in HN. It's very disappointing.
984.
by gnulinux 6y ago
Nope, I'm not from China or India (so I'm in the global pool). If you're from India, it's impossible to get citizenship this way (the waitlist is too long), you need to marry a US citizen if you want citizenship.
985.
by gnulinux 6y ago
What you're missing is this is affecting all students in Georgia Tech, Harvard, MIT etc as well.
986.
by gnulinux 6y ago
Going from a student with F visa to Green Card is a >10 year adventure with all sorts of problems and complex legal framework. Not to mention, it's practically impossible for some majors, in particular if your major does not apply t
987.
by gnulinux 6y ago
> the US is still extremely generous with immigration. US is the WORST country on earth for immigration. I came to US >10 years ago, still NOWHERE near getting a Green Card. Will probably won't get well into my 30s or 40s. It&#x2
988.
by gnulinux 6y ago
I should add that even if you have the technology to prove correctness of program, that doesn't mean it's practical to prove correctness of all behavior of the program. I write real life programs in Agda (which is a dependently
989.
by gnulinux 6y ago
I'm not sure what you're trying to say? Bool can have 2 states, but in software we need things that have 3, 4 or N states too. So we need an abstraction that is like Bool but can have any number of cases. Moreover, bool is clearly
990.
by gnulinux 6y ago
This is why I still use Python in performance critical code (but not so performance critical that you need to squeeze each CPU cycle). It's simply too easy to write performance critical functions in C and ffi call it in python. Of co

More ›