4 ms·

For lambda calculus, the motto is "when everything is a function". The boolean true is the function λx.λy.x, while false is λx.λy.y. If b then x else y then sim

by tromp 1y ago

For lambda calculus, the motto is "when everything is a function". The boolean true is the function λx.λy.x, while false is λx.λy.y. If b then x else y then simply becomes b x y. In a functional language like Haskell that is basically a typed lambda calculus with lots of syntactic sugar, we can replicate this with: type MyBool a = a -> a -> a myTrue :: MyBool a myTrue = \x y -> x myFalse :: MyBool a myFalse = \x y -> y myIf :: MyBool a -> a -> a -> a myIf b myThen myElse = b myThen myElse main = print $ myIf myTrue "true" "false"

Y_Y 1y ago
yourIf == myId
- tromp 1y ago
  No instance for (Eq (MyBool a0 -> a0 -> a0 -> a0)) arising from a use of ‘==’ Undecidability of function equality aside, we could indeed define "myIf = id" instead.
  - Y_Y 1y ago
    Fair point, though if I remeber correctly there is only one function with type a->a and so we get equality automatically. (This may be untrue in the presence of the likes of unsafeCoerce.)
    - tromp 1y ago
      There are other functions MyBool a -> MyBool a, such as not = \b x y -> b y x.
nextaccountic 1y ago
This is https://en.wikipedia.org/wiki/Church_encoding#Church_Booleans https://en.wikipedia.org/wiki/Church_encoding#Church_Boolean... But there are other encodings
- tromp 1y ago
  This is both the Church encoding and the Scott encoding of the abstract data type data Bool = True | False making it pretty much the only encoding you find in the literature. This is quite different from the case of the natural numbers, where not only do the Church and Scott encoding differ, but there are several other reasonable representations fitting particular purposes.