Puzzle #10 Discussion

[vlad2048]

Puzzle 10

I got to level 10, but I think the "If" implementation is not working. Or it could very well be me. The editor tells me:

• True(n, n) is a valid expression (it returns n). But not using all the functions. Makes sense
• If(True, n, n) Argument type mismatch!

given the definition of If: (p, a, b) => p(a, b) I don't understand why the second expression gives an argument mismatch ? it should be directly equivalent to the first

[vlad2048]

After some more experimenting, I found that n => If(GreaterThan, True, False)(n,n) is valid (and the solution quickly followed) So "If" takes (for lack of better words), a level 2 function and two level 1 functions Still confused why my initial expression is not valid as I thought lambda calculus was all about plain substitutions

[RxDave]

Congrats for solving it!

Still confused why my initial expression is not valid as I thought lambda calculus was all about plain substitutions

The underlying types still matter though. A higher-order system would allow you to pass in a function that represents a number, for example, but that doesn't mean that you can just pass in a number directly when a function is expected.

Check out "Church Numeral" and "Church Boolean" on the web for related ideas.

More details:: Although your initial concept matches, the underlying types do not. A piece's definition can imply some information about its type. Part of the puzzle is in solving what the underlying types of each piece actually are, and therefore how they compose.

True is of the type (x, y) => x, whereby x and y are specific types themselves. If is of the type (p, a, b) => p(a, b), whereby p, a and b are also specific types.

The puzzle does not indicate the types of x, y, p, a and b. Part of solving this puzzle is in solving those types.

Experimenting with True(n, n), as you did, revealed the underlying types of x and y. Therefore, you now know the complete type of True.

Experimenting with If(True, n, n) was a great follow-up idea. The argument type mismatch indicates that p is not the same type as True, or that n is not the same type as a, or n is not the same type as b, or some combination of the three has incorrect types.

From there you worked out what the types had to be, implicitly, to solve the puzzle. Sometimes process of elimination helps a lot here because there aren't very many permutations, or at least you can often eliminate a bunch right away based on the limited type information you can infer from the pieces' definitions!

[vlad2048]

Thank you so much for the detailed explanation. I need to deduce the implicit types, this makes sense, I'll try puzzle #11 again. Nice idea and implementation by the way. (no luck hacking at the html:)

[RxDave]

Haha glad to know, thanks :-) You may want to back up your cookie because that's where your game is saved. I feel bad if players have lost their state on accident, probably one reason why not a lot of people are interested in trying the puzzles. I don't blame them. Maybe one day I'll add server accounts :/