chriskrycho + haskell   5

The Great Theorem Prover Showdown —Hillel Wayne “Functional programming and immutability are hot right now. On one hand, this is pretty great as there’s lots of nice things about functional programming.”
Functional programming and immutability are hot right now. On one hand, this is pretty great as there’s lots of nice things about functional programming. On the other hand, people get a little overzealous and start claiming that imperative code is unnatural or that purity is always preferable to mutation.

I think that the appropriate paradigm is heavily dependent on context, but a lot of people speak in universals. I keep hearing that it’s easier to analyze pure functional code than mutable imperative code. But nobody gives rigorous arguments for this and nobody provides concrete examples. Nobody actually digs into why assignments and transitions are so much harder to reason about than pure functions and IO monads. We’re just supposed to accept it as an axiom.

I don’t like accepting things as axioms. If we make a claim, we better damn well put it to the test.
hillel-wayne  dafny  fp  type-theory  programming  haskell  idris  agda  ip  computer-science  fstar  theorem-proving 
june 2018 by chriskrycho
Three Months of Go (from a Haskeller's perspective)
I will probably never choose to use Go for anything ever again, unless I’m being paid for it. Go is just too different to how I think: when I approach a programming problem, I first think about the types and abstractions that will be useful; I think about statically enforcing behaviour; and I don’t worry about the cost of intermediary data structures, because that price is almost never paid in full.
go  plt  haskell 
march 2017 by chriskrycho
From OOP to FP - Inheritance and the Expression Problem
The "expression problem" and ADTs vs. extensible types (e.g. open/closed principle):
Of course, we did not solve the expression problem, but thanks to the fact that we can handle functions as data in FP, at least we can now choose which side of the problem we want to face. We can have our desired comfort for software that often gets new types and rarely new functions, despite the presence of a stong static type system. We now can invent hundreds of new subtypes like baz and qux and easily add them to our world. We do not have to edit central monster functions for the actions of all the different types. Everything is neatly arranged in the modules of the actual type.
haskell  elm  programming  open-closed-principle  software-development  fp  oop 
march 2017 by chriskrycho
Retrofitting Linear Types
Bernardy, Boespflug, Newton, Peyton Jones & Spiwack: Retrofitting Linear Types
plt  linear-types  haskell  from twitter_favs
march 2017 by chriskrycho

Copy this bookmark:



description:


tags: