freyrs3

10 ms·

61.
by freyrs3 12y ago
Types are the world's most popular verification technique. The whole intent of types is to automate many of the proofs required to guarantee the correctness of the program rather than having the human operator get bogged down in verify
62.
by freyrs3 12y ago
There's a lot of study in psychology about how our mental models of our future selves result in the choices in we make in the present. I know quantifiably from having worked in a both ML family languages and the popular dynamic scripti
63.
by freyrs3 12y ago
You can however obligate that the function that invokes the outside IO be required to return valid input as a constraint in the type-system. So you wouldn't be able to compose an unrestricted ``readLine`` function with a function that
64.
by freyrs3 12y ago
Conceptually they are similar, though it's always important to note that C++ has several man-centuries worth of compiler work. Rust may become stable and efficient enough to replace some existing C++, but at the moment it's most c
65.
by freyrs3 12y ago
> you gain almost nothing from Haskell, and you might have been better off writing your code in another language. Don't know about that. Even if you write everything in the IO monad, Haskell is still a pretty great imperative langua
66.
by freyrs3 12y ago
Though if you take this intuition too far it tends to break down, for instance IO and ST both define functor instances but it doesn't really make sense to talk about a functor over IO preserving shape.
67.
by freyrs3 12y ago
> you can multiply n by k, k by m matrices to get an n by m matrix, but anything else is a type error. This is exactly how Repa works, it uses a Peano encoding of the extent of dimensions to make invalid array operations inexpressible.
68.
by freyrs3 12y ago
It's a great read indeed. If anyone is interested in more concrete applications of Haskell then a read through this should be enough to convince anyone that we can do some really amazing parallel programming on top of Haskell's RT
69.
by freyrs3 12y ago
> I'm pretty sure that it is possible to make a function in Haskell which, while it mutates variables, these variables are all local, so you are still able to offer up a purely functional interface to the world outside of that funct
70.
by freyrs3 12y ago
It was originally part of the authors PhD work, it hasn't been touched since he graduated.
71.
by freyrs3 12y ago
The map example with toplevel pattern matching is really just sugar for the expanded case statements which isn't that far from the Ur equivalent. map :: forall a b. (a -> b) -> [a] -> [b] map = \ (@ a) (@ b) (ds :: a
72.
by freyrs3 12y ago
Because type systems, at least in the ML tradition, reduce down to systems of logic that we already know how to prove properties about. We can prove progress and preservation of a type system, and we even have systems to mechanically check
73.
by freyrs3 12y ago
Coq is first and foremost a proof assistant, you can construct theorems in types and inhabitants of those types constitute proofs of theorems. it's based on a much more advanced type system called the Calculus of Constructions[1]. Coq
74.
by freyrs3 12y ago
Do you assemble your own machine code as well or do you trust that someone else has taken care of the gritty details of the assembler so that you can work at a level of abstraction higher than that?
75.
by freyrs3 12y ago
Humans are humorously bad at reasoning about large software systems written by a large number of people. Even if all the code you personally write is locally safe, it's very very difficult to guarantee that the interaction of it with a
76.
by freyrs3 12y ago
This code here isn't representative of any Haskell end-users would write, it has a whole other syntax (LiquidHaksell) layered on top of it that augments the type system and it imports the internals of GHC.* libraries to work with the b
77.
by freyrs3 12y ago
The problem to solve world hunger is to be able to distribute staple crops more efficiently to places which don't have access to existing markets. There's no conceivable way that some highly refined meal-replacement product for th
78.
by freyrs3 12y ago
I don't understand why Soylent receives the press it does, meal-replacement shakes have been on the market for quite a long time. The entire phenomenon seems to just be a marketing gimmick around some misguided notion of it "repla
79.
by freyrs3 12y ago
Unfortunately weak typing is still a very ill defined term and is somewhat misleading because it tends to carry a lot of implicit assumptions about which type coercions are expected. Implicit conversion between floating point and integral t
80.
by freyrs3 12y ago
Every language that differs from the structure you're familiar with will seem crazy until you learn how to read it. Be that Haskell, Erlang or Japanese it's no different.
81.
by freyrs3 12y ago
Yes, it's pretty universal that people find it uncomfortable to force themselves to think in a language they don't fully understand yet. Whether that's Ruby, Haskell, or Japanese. There are plenty of valid things to compare l
82.
by freyrs3 12y ago
Well I mean, there is a lot of utility in programming with categorical concepts in Haskell. There's plenty of libraries in the Haskell ecosystem that wouldn't even exist if it weren't for drawing upon category theory for guid
83.
by freyrs3 12y ago
For those interested in a little more rigor, there's a great series of lectures on the subject that was just posted online from Steve Awodey, who wrote one of the best introductory texts on the subject. https://www.youtube.c
84.
by freyrs3 12y ago
The examples the author chose are kind of hand-wavy, unix pipes in full are obviously not categories. But I recognize how hard is to come up with examples that aren't contrived and that programmers can relate to without knowing much ma
85.
by freyrs3 12y ago
Nothing is wrong with it, it's just as relevant today as it was 40 years ago, if not more. Most of the really interesting modern work is just building on top of some form intensional Martin-Löf theory.
86.
by freyrs3 12y ago
Both System-F and Martin-Löf type theory are roughly 40 years old as well.
87.
by freyrs3 12y ago
Boxing and memory locality are the the main bottlenecks in scientific computations with Python, dynamic typing is orthogonal.
88.
by freyrs3 12y ago
What kind of examples are you interested in?
89.
by freyrs3 12y ago
(^.) is a really simple function actually, I'd argue it's even simpler than fmap. If we look at `lens-family-core` all the machinery to derive everything you need to make lenses is very concise and would fit on a index card. http
90.
by freyrs3 12y ago
If you work with Java/C/C++ then the way you structure, compose, and think about programs is mostly entirely different from Haskell. Any of the examples I might point to as idiomatic Haskell are going to be "unreadable"

More ›