←back to thread

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

(ezzeriesa.notion.site)
389 points kurinikku | 1 comments | 17 Nov 24 15:07 UTC | HN request time: 0.234s | 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 #
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 #
1. 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.