←back to thread

Everything Is Just Functions: 1 week with David Beazley and SICP

(ezzeriesa.notion.site)
389 points kurinikku | 3 comments | 17 Nov 24 15:07 UTC | HN request time: 0.406s | source
Show context
marvinborner ◴[17 Nov 24 16:10 UTC] No.42164919[source]▶
They give a nice introduction to encoding state as pure functions. In fact, there are many more purely functional encodings for all kinds of data like trees, integers, sum/product types, images, monads, ...

The encodings can be a bit confusing, but really elegant and tiny at the same time. Take for example a functional implementation of the Maybe monad in javascript:

  Nothing = nothing => just => nothing
  Just = v => nothing => just => just(v)
  
  pure = Just
  bind = mx => f => mx(mx)(f)
  
  evalMaybe = maybe => maybe("Nothing")(v => "Just " + v)
  console.log(evalMaybe(bind(Nothing)(n => pure(n + 1)))) // Nothing
  console.log(evalMaybe(bind(Just(42))(n => pure(n + 1)))) // Just 43
replies(5): >>42166462 #>>42166688 #>>42166841 #>>42168370 #>>42173549 #
SkiFire13 ◴[17 Nov 24 20:03 UTC] No.42166688[source]▶
You can see this as replacing an inductive type with its recursor's function type. It's pretty cool in type theory, but not so good for actually programming stuff.
replies(1): >>42169698 #
1. gleenn ◴[18 Nov 24 04:23 UTC] No.42169698[source]▶
Honest question: why is that bad for actual programming stuff? Is it because the type theory is interesting but doesn't really help? Performance?
replies(2): >>42171192 #>>42173532 #
2. jrvieira ◴[18 Nov 24 10:19 UTC] No.42171192[source]▶
i am guessing that most people think that the cognitive load cost is usually not worth the benefits.

i agree that the cognitive load in a language like js which is not prepared to accommodate this paradigm is not worth it

even when deciding to use Haskell we need to weigh the pros and cons wrt the project's goals

3. SkiFire13 ◴[18 Nov 24 15:52 UTC] No.42173532[source]▶
In this particular case IMO it's bad because it essentially removes nominal typing for arguably no benefit.

Even in Lean, a dependently typed language where recursors can be made explicit, people prefer using pattern matching instead of them. There is even sugar for transforming some recursors-like functions into pattern matching like syntax. FYI in Lean recursors are marked as non-computable due to performance concerns, so you can use them to write proofs but not programs.

Seen from yet another point of view, this is transforming inductive types in a function corresponding to a visitor. And yet functional programming folks spent years trying to convince people to replace visitors with proper inductive/algebraic data types and pattern matching, so this idea is a step backwards even for them.