5 ms·

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, in

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

hinkley 2y ago
[flagged]
- 6510 2y ago
  If there is a wrong way to do something someone will do it.
  - hinkley 2y ago
    There’s an old saying attributed to the Inuit: everyone enjoys the smell of their own farts.
- marvinborner 2y ago
  I think it's all right if you're used to the notation. The first two lines are tagged unions and will be recognisable as such if you're familiar with encodings like Scott/Church pairs/lists/numbers. Once you understand the structure, the definition of `bind` becomes obvious, as its two arguments represent the cases "is nothing" and "is just", where in the first case Nothing is returned, and in the second case the function is applied to the value inside the Just. I think that writing such code, if only for educational purposes, can be really helpful in actually understanding how the state "flows" during the monadic bind/return. Typical monad instantiations of Maybe do not give such deep insight (at least to me). > Just because you can do a thing doesn’t mean you should. Of course you should, where would be the fun in that?
  - salawat 2y ago
    >I think it's all right if you're used to the notation. Higher mathematics in a nutshell. >Of course you should, where would be the fun in that? Also higher mathematics in a nutshell. Narrator asks: Who should we put in charge of <<thing that will effect people in a tangible way>>? Not the mathematicians! echo the crowd in unanmity. Narrator asks: Who will we delegate the task of <<abuse of notation>> to? The crowd grumbles, arguing amongst themselves whether such a question even warrants an answer. A mathematician stands up, proclaiming "We'll take it!", following up with, "Once you understand the notation involved in my previous statement, you will understand why this outcome is inevitable." The crowd, seeing the wisdom of not even embarking on that tribulation, assents to the delegation, given the task of undoing the abuse of notation for the legibility of the layperson is also delegated to the aspiring mathematician. Scene opens on current day...
  - tmtvl 2y ago
    > The first two lines are tagged unions Are they? But in the Nothing you have 2 identical members (`nothing' without arguments), won't that throw an exception? To borrow Rust syntax (pun intended): enum Nothing { nothing, just nothing }; That's just weird.
    - marvinborner 2y ago
      When encoding tagged unions as lambdas, the tags are arguments. In this case `Nothing` has two available tags (`nothing` and `just`) and uses the tag `nothing`. `Just` does the same with the tag `just`, only that the tag gets an additional argument (as does its constructor `Just`), such that the value can be extracted afterwards - just like in an enum: enum Maybe<T> { Nothing, Just(T), }
    - ezwoodland 2y ago
      [dead]
  - IshKebab 2y ago
    It's alright once you get used to it usually means it isn't alright in my experience. There are exceptions of course.
- deleted 2y ago
  [deleted]
- williamcotton 2y ago
  It’s definitely easier to read in an ML language, that’s for sure!
SkiFire13 2y ago
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.
- gleenn 2y ago
  Honest question: why is that bad for actual programming stuff? Is it because the type theory is interesting but doesn't really help? Performance?
  - jrvieira 2y ago
    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
  - SkiFire13 2y ago
    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.
solomonb 2y ago
You can derive these implementations from the recursion principle for your type: data Maybe a = Nothing | Just a foldMaybe :: (Unit -> r) -> (a -> r) -> Maybe a -> r The two higher order functions passed into `foldMaybe` are your `Nothing` and `Just` (modulo I added the Unit param to the Nothing case to be a little more precise).
- gugagore 2y ago
  If you have any light to shed, I'm wondering about inductive data types and their expressive necessity here: https://news.ycombinator.com/item?id=42166709 https://news.ycombinator.com/item?id=42166709
akira2501 2y ago
It may be elegant mathematically, but then conveyed through a language that is strictly in the ASCII character set without any alignment or internal justification, they're really just painful to look at.
tempodox 2y ago
In short, the untyped lambda calculus is Turing-complete.

hinkley 2y ago

[flagged]

6510 2y ago
If there is a wrong way to do something someone will do it.
- hinkley 2y ago
  There’s an old saying attributed to the Inuit: everyone enjoys the smell of their own farts.
marvinborner 2y ago
I think it's all right if you're used to the notation. The first two lines are tagged unions and will be recognisable as such if you're familiar with encodings like Scott/Church pairs/lists/numbers. Once you understand the structure, the definition of `bind` becomes obvious, as its two arguments represent the cases "is nothing" and "is just", where in the first case Nothing is returned, and in the second case the function is applied to the value inside the Just. I think that writing such code, if only for educational purposes, can be really helpful in actually understanding how the state "flows" during the monadic bind/return. Typical monad instantiations of Maybe do not give such deep insight (at least to me). > Just because you can do a thing doesn’t mean you should. Of course you should, where would be the fun in that?
- salawat 2y ago
  >I think it's all right if you're used to the notation. Higher mathematics in a nutshell. >Of course you should, where would be the fun in that? Also higher mathematics in a nutshell. Narrator asks: Who should we put in charge of <<thing that will effect people in a tangible way>>? Not the mathematicians! echo the crowd in unanmity. Narrator asks: Who will we delegate the task of <<abuse of notation>> to? The crowd grumbles, arguing amongst themselves whether such a question even warrants an answer. A mathematician stands up, proclaiming "We'll take it!", following up with, "Once you understand the notation involved in my previous statement, you will understand why this outcome is inevitable." The crowd, seeing the wisdom of not even embarking on that tribulation, assents to the delegation, given the task of undoing the abuse of notation for the legibility of the layperson is also delegated to the aspiring mathematician. Scene opens on current day...
- tmtvl 2y ago
  > The first two lines are tagged unions Are they? But in the Nothing you have 2 identical members (`nothing' without arguments), won't that throw an exception? To borrow Rust syntax (pun intended): enum Nothing { nothing, just nothing }; That's just weird.
  - marvinborner 2y ago
    When encoding tagged unions as lambdas, the tags are arguments. In this case `Nothing` has two available tags (`nothing` and `just`) and uses the tag `nothing`. `Just` does the same with the tag `just`, only that the tag gets an additional argument (as does its constructor `Just`), such that the value can be extracted afterwards - just like in an enum: enum Maybe<T> { Nothing, Just(T), }
  - ezwoodland 2y ago
    [dead]
- IshKebab 2y ago
  It's alright once you get used to it usually means it isn't alright in my experience. There are exceptions of course.
deleted 2y ago
[deleted]
williamcotton 2y ago
It’s definitely easier to read in an ML language, that’s for sure!

SkiFire13 2y ago

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.

gleenn 2y ago
Honest question: why is that bad for actual programming stuff? Is it because the type theory is interesting but doesn't really help? Performance?
- jrvieira 2y ago
  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
- SkiFire13 2y ago
  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.

solomonb 2y ago

You can derive these implementations from the recursion principle for your type: data Maybe a = Nothing | Just a foldMaybe :: (Unit -> r) -> (a -> r) -> Maybe a -> r The two higher order functions passed into `foldMaybe` are your `Nothing` and `Just` (modulo I added the Unit param to the Nothing case to be a little more precise).

gugagore 2y ago
If you have any light to shed, I'm wondering about inductive data types and their expressive necessity here: https://news.ycombinator.com/item?id=42166709 https://news.ycombinator.com/item?id=42166709

akira2501 2y ago

It may be elegant mathematically, but then conveyed through a language that is strictly in the ASCII character set without any alignment or internal justification, they're really just painful to look at.

tempodox 2y ago

In short, the untyped lambda calculus is Turing-complete.