Types and Programming Languages (MIT Press)

Category: Programming
Author: Benjamin C. Pierce
4.0
This Month Hacker News 1

Comments

by wcrichton   2018-09-25
Strongly recommend Types and Programming Languages [1]. I think it's the most useful + accessible book on type theory out there.

[1] https://www.amazon.com/Types-Programming-Languages-MIT-Press...

by anonymous   2017-08-20

So, @PetSerAl is absolutely right that the correct answer to this (if we are looking for a lambda-calculus-esque solution) is:

(define not
  (lambda (b)
    (lambda (x y) (b y x))))

Thus: ((not true) 1 2) gives 2 and ((not false) 1 2) gives 1.

But since you didn't specify lambda calculus in your question, but instead tagged both Racket and Scheme, I will give you an answer that works there.

Consider if you have true and false defined as above. Then writing not is as simple as:

(define not
  (lambda (x)
    (cond [(equal? x true) false]
          [(equal? x false) true]
          [else (error "Value is not true or false")])))

This has the same semantics listed above: ((not true) 1 2) gives 2 and ((not false) 1 2) gives 1. But it has the added benefit that you can actually directly examine it to see the value, rather than just applying it to another procedure. For example:

> (not true)
#<procedure false>
> (not false)
#<procedure true>

You can even now use equal? (or really eq? on them), whereas before you would have always gotten #f if you tried that:

> (equal? (not true) false)
#t
> (equal? (not true) true)
#f
> (equal? (not false) true)
#t
> (equal? (not false) false)
#f

This leads to a whole discussion of PL theory about what can and cannot be decided with the lambda calculus. That I will elide here. But if you are interested, I recommend you check out this book, or that book.