9 ms·

This comment and the parent comment was really interesting. It's made me think about my current path and somethings I have done/learned that has incrementally p

by jwdunne 11y ago

This comment and the parent comment was really interesting. It's made me think about my current path and somethings I have done/learned that has incrementally pushed me towards functional programming over a long window of time. I have played with Scheme, along with a half-completed SICP read through. I have also played with Haskell, along with partial read throughs of LYAH and real-world Haskell. Those experiences, although incomplete, have been important to me as a programmer. I don't think those actually 'sold' me on FP though. I took a detour for some time and decided to become a better programmer using OO methodologies. I used TDD, I memorised SOLID and all that. Read up on design patterns and then used them practically. All well and good. From my toying with Scheme, Haskell and associated literature, I wasn't entirely satisfied. The code I produced was always a bit, I'm not sure, but not entirely satisfiying. It looked and worked better than what I get given to review when considering freelancers for an extra pair of hands - part of that is because of PHP I think. I carried on this way for a while in any case. In my own self-learning, I'd started looking at language design and compilers. I read some books and decided I didn't have enough mathematical skills to consume the texts. I turned to learning discrete mathematics. That was a big eye opener. As I was reading about formal logic, set theory, proofs, etc, my mind kept turning to the problem of applying this in my work. Haskell and FP came to mind too. I believe doing this helped it finally click that a functional approach can be taken successfully in most of the work I do. Whilst I was doing this, I had a fairly simple project that, if designed correctly, could make my life easier in future projects. I took an OO approach, designed the UML, started writing tests, etc. I decided that it was over-engineered or at least it was a lot of work for what I was trying to do. I decided to take an FP approach. I had the project completed with far less code that I was happier with. In the same language. That was almost like an 'epiphany moment'. I started getting seriously interested about functional programming then. I am now starting to see the flaws and bloat in the approaches I was taking before. I recently read Out of the Tar Pit again. I had read it before but I didn't really get it. This time it excites me and made my brain whir with ideas. Especially on how I can make these approaches compatible with the constraints of my day job. I actually now digest as much as I can about FP. Haskell, as an important player, frequently comes up. After laying the ground work, monads make a lot more sense. Haskell as a language excites me. In my opinion, and I am self-taught when it comes to computers so it may not be 100% applicable, here is what I did to start my transition from imperative to declarative: a) experiment with functional programming. Not actually get it and be ok with that. Carry on down the path. b) Read HN and note articles posted about FP c) Continue learning about imperative programming and consume the advice from OO thought leaders. Apply it to your work. d) Learn a bit about maths and what it actually is, especially realising it's not just rote computation and application of algorithms from school. e) Take a functional approach instead of an OO approach within the language you are working with. I did this in PHP. Not only will it show you how FP compares, it will also show you why Haskell/OCaml/etc by way of the deficiencies for FP in your chosen languages. In PHP, the type system (arrays as your Everyman...) and inconsistent type hints, explicit closing over of variables in outer scopes and piss-poor support for modules is one. Biggest is the only way to pass a function in the function namespace is to use a a fully-qualifies string (so function name along with namespace - you get undefined constant otherwise). With Java, it might be that you cannot have stand alone functions, which would suck. This helped a lot for me but I'm sure spending a long time learning about software down to the hardware in my spare time contributed a lot to this too.

mbrock 11y ago
Nice to hear. I had similar moments of epiphany while taking a course on abstract algebra and writing down some theorems in the form of Agda definitions. As you may know, Agda is a Haskell-inspired language that has an even more powerful type system that makes it possible to define arbitrarily strong types, so that for instance you can define the type of a function that sorts a list—and then know confidently that any implementation of that type does indeed sort a list. Anyway, when learning Agda, one comes across the notion that programs and proofs are in some sense the same thing. In other words that the code for a function can be read as a proof that the type of that function is inhabited. This seemed to me kind of bizarre and magical at first... The more I thought about it, the more it made real sense, and not only that, it helped me understand proofs in a much more intuitive way. Before, if you had asked me what a proof is, I might have said "it's a very strict way to argue that a statement really is true." I didn't know that such proofs can be given formal structure... I couldn't really explain how to relate it to programming or functions... But now that I've to some degree internalized the notion, if you ask me what a proof is, I might say it's an unambiguous description of how to transform an input into an output. If you call the input P and the output Q, then P is a premise and Q is a conclusion, and the proof is the "arrow" P -> Q that through some well-defined sequence of "truth-preserving transformations" gives you knowledge of Q assuming nothing but P (and some fundamental axioms). And in the world of programming, P is an input argument and Q is a resulting value, while the "arrow" P -> Q is a well-defined sequence of correct transformation that produces a Q-value given only a P-value (and some fundamental primitive functions). So in this sense you can say that the implementation of a function is actually a kind of logical argument. If you want to make use of this insightful connection (the "Curry-Howard equivalence"), however, your programming language needs to be pretty strict. If your P -> Q argument suddenly throws a null pointer exception, it's not much of an argument—it means your claim of being able to produce a Q given P is false. This connection really helped me to understand both proofs and programs in a deeper way.
- jwdunne 11y ago
  Thank you. 1. I'd heard of Agda but never read any code. What a brilliant language. I've added it to my list of my languages to spend time with. 2. I think your experience with Agda, especially the realisation that programs = proofs, leading to the Curry-Howard correspondence is exciting and rightfully bumps Agda to the top of my list. Functional programming has also opened my eyes with type systems too. That actually, an inconsistent and weak type system is a bigger liability than once thought - I'm realising that daily. Especially with null values and "trying to call method on non-object" errors.

by jwdunne 11y ago

mbrock 11y ago

Nice to hear. I had similar moments of epiphany while taking a course on abstract algebra and writing down some theorems in the form of Agda definitions. As you may know, Agda is a Haskell-inspired language that has an even more powerful type system that makes it possible to define arbitrarily strong types, so that for instance you can define the type of a function that sorts a list—and then know confidently that any implementation of that type does indeed sort a list. Anyway, when learning Agda, one comes across the notion that programs and proofs are in some sense the same thing. In other words that the code for a function can be read as a proof that the type of that function is inhabited. This seemed to me kind of bizarre and magical at first... The more I thought about it, the more it made real sense, and not only that, it helped me understand proofs in a much more intuitive way. Before, if you had asked me what a proof is, I might have said "it's a very strict way to argue that a statement really is true." I didn't know that such proofs can be given formal structure... I couldn't really explain how to relate it to programming or functions... But now that I've to some degree internalized the notion, if you ask me what a proof is, I might say it's an unambiguous description of how to transform an input into an output. If you call the input P and the output Q, then P is a premise and Q is a conclusion, and the proof is the "arrow" P -> Q that through some well-defined sequence of "truth-preserving transformations" gives you knowledge of Q assuming nothing but P (and some fundamental axioms). And in the world of programming, P is an input argument and Q is a resulting value, while the "arrow" P -> Q is a well-defined sequence of correct transformation that produces a Q-value given only a P-value (and some fundamental primitive functions). So in this sense you can say that the implementation of a function is actually a kind of logical argument. If you want to make use of this insightful connection (the "Curry-Howard equivalence"), however, your programming language needs to be pretty strict. If your P -> Q argument suddenly throws a null pointer exception, it's not much of an argument—it means your claim of being able to produce a Q given P is false. This connection really helped me to understand both proofs and programs in a deeper way.

jwdunne 11y ago
Thank you. 1. I'd heard of Agda but never read any code. What a brilliant language. I've added it to my list of my languages to spend time with. 2. I think your experience with Agda, especially the realisation that programs = proofs, leading to the Curry-Howard correspondence is exciting and rightfully bumps Agda to the top of my list. Functional programming has also opened my eyes with type systems too. That actually, an inconsistent and weak type system is a bigger liability than once thought - I'm realising that daily. Especially with null values and "trying to call method on non-object" errors.