The Little Typer Exercise 3.4

Exercise 3.4.rkt

#lang pie

(claim >
  (-> Nat Nat Nat))
(define >
  (lambda (n)
    (rec-Nat n
      (the (-> Nat Nat) (lambda (m) 0))
      (lambda (n-1 n-1>)
        (lambda (m)
          (rec-Nat m
            1
            (lambda (m-1 _)
              (n-1> m-1))))))))

(claim max
  (-> Nat Nat Nat))
(define max
  (lambda (n m)
    (rec-Nat (> n m)
      m
      (lambda (_ _) n))))

(check-same Nat 0 (max 0 0))
(check-same Nat 1 (max 1 0))
(check-same Nat 1 (max 0 1))
(check-same Nat 2 (max 2 1))
(check-same Nat 2 (max 1 2))

The code for > is very strange. I came up with it by first considering the functions 0>, 1> and 2>. That is, the functions that compute 0 > n, 1 > n and 2 > n. Then abstracted that to n> that computes n > m. Then I realised that n> was just the curried form of >, so ((>n n) m) became simply (> n m).

I figured out a direct solution.

#lang pie

(claim max
  (-> Nat Nat Nat))
(define max
  (lambda (n)
    (rec-Nat n
      (the (-> Nat Nat)
        (lambda (m) m))
      (lambda (n-1 max/n-1)
        (lambda (m)
          (rec-Nat m
            (add1 n-1)
            (lambda (m-1 _)
              (add1 (max/n-1 m-1)))))))))

(check-same Nat 0 (max 0 0))
(check-same Nat 1 (max 1 0))
(check-same Nat 1 (max 0 1))
(check-same Nat 2 (max 2 1))
(check-same Nat 2 (max 1 2))

Nice! Below is a minor rewrite of your direct solution (which merely uses which-Nat and factors out add1). What I was not able to do is introduce m from the start (i.e., (define max3 (λ(n m) TODO))); I would be interested in knowing whether it's possible.

(claim id-Nat (-> Nat
                  Nat))
(define id-Nat (λ(n) n))

(claim max3 (-> Nat Nat
                Nat))

(define max3
  (λ(n)
    (rec-Nat n
      id-Nat
      (λ(n-1 f m)
        (add1 (which-Nat m n-1 f))))))

Cool!

Factoring out add1 is neat.

We learnt early on whilst studying The Little Typer that introducing too many variables at the start often caused problems.

My mathematician friend tells me it has something to do with "making the inductive hypothesis too weak". I can't say I have fully understood what that means, but what I can tell you is that by introducing fewer variables at the start you can let the later variables vary with respect to the earlier and make the inductive hypothesis you obtain more flexible and thus more useful.

Although the above example does not use ind-Nat, I think something similar is happening.

I think it is impossible to define this function by introducing both n and m.

Hope that helps.

I agree. I too suspect that it's not possible to introduce m at the start . For what it's worth it seems similar to an issue I encountered when using another dependently typed language called Lean, and a tactic called revert. You can read a discussion of it on the Lean Zulip archive (my contribution to the discussion was to observe that "I also found the use of revert ... tricky").

Thanks for the pointers.

You may be interested in this group https://www.meetup.com/London-TyDD, if you are based in London.

I would be, but unfortunately I am not — I’m in NYC.

…

On Mon, Feb 3, 2020 at 7:48 AM aymanosman ***@***.***> wrote: Thanks for the pointers. You may be interested in this group https://www.meetup.com/London-TyDD, if you are based in London. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <https://gist.github.com/9db1db11755ef4b4759c4ee9a4bdb515?email_source=notifications&email_token=AAABM3JIFCKQI2R7VTD5CXTRBAHBPA5CNFSM4KLSD4OKYY3PNVWWK3TUL52HS4DFVNDWS43UINXW23LFNZ2KUY3PNVWWK3TUL5UWJTQAGBFAC#gistcomment-3164673>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAABM3KLL6CMNI427F3ZRRDRBAHBPANCNFSM4KLSD4OA> .