1
$\begingroup$

In this question, I am talking about the language Pie described in the book The Little Typer.

Consider the definition

(claim foo-or-bar (-> Nat Atom Atom))
(define foo-or-bar
  (λ (n) (ind-Nat n
           (λ (n) (-> Atom Atom))
           (λ (a) 'foo)
           (λ (n-1 result_n-1 a) 'bar))))

If I then type foo-or-bar on a separate line and execute, Pie outputs

(the (→ Nat Atom
       Atom)
  (λ (n x₁)
    ((ind-Nat n
        (λ (n₁)
          (→ Atom
            Atom))
        (λ (a)
          'foo)
        (λ (n-1 result_n-1 a)
          'bar))
      x₁)))

So, Pie says that the second code snippet is the normal form of foo-or-bar. It's pretty clear why

(λ (n x₁)
  ((ind-Nat n
     (λ (n₁)
       (→ Atom
         Atom))
     (λ (a)
       'foo)
     (λ (n-1 result_n-1 a)
       'bar))
    x₁))

is the same (-> Nat Atom Atom) as

(λ (n) (ind-Nat n
           (λ (n) (-> Atom Atom))
           (λ (a) 'foo)
           (λ (n-1 result_n-1 a) 'bar)))

It's by The Final Second Commandment of lambda, which says

If f is a (Pi ((y Y)) X), and y does not occur in f, then f is the same as (lambda (y) (f y)).

But The Little Typer say that the normal form of an expression is the most direct way of writing it. And, frankly, what I wrote in the definition of foo-or-bar seems more direct than what Pie says its normal form is. So, why is that the normal form? I remember the book said somewhere that if f is a neutral expression of a Pi type, then (lambda (x) (f x) is the normal form of f. This seems similar to the situation with foo-or-bar but not directly applicable.

$\endgroup$

1 Answer 1

2
$\begingroup$

There are 2 questions here.

The first one is whether the situation is applicable. In fact it is! This is because $(\lambda (x\ y)\ f)$ is abbreviation for $(\lambda (x)\ (\lambda (y)\ f))$. So you apply that in the inner layer.

The second question is why $(\lambda (x)\ (f\ x))$ is more "direct" than $f$. This is because $\lambda$ is the only way to create a $\Pi$ type. Thus it would be more direct to explicitly convey this knowledge. Remember that "direct" doesn't mean short or concise. For example, 10000000000 is a much more direct way to write $10^{10}$ but it is much longer.

The Little Typer chose to use a more blurry definition. But in practice it is well-defined. Only when the type is $\mathbb N, A+B, \mathcal U$, should a neutral term of that type be normal.

$\endgroup$
9
  • 1
    $\begingroup$ I think I understand now. If n is a variable of type Nat, and thus a neutral expression, is (ind-Nat n (λ (n) (-> Atom Atom)) (λ (a) 'foo) (λ (n-1 result_n-1 a) 'bar))) a neutral expression? Yes, by the box "Neutral expressions" in ch. 8. What is its type? Its type is (Pi ((a Atom)) Atom. What is its normal form? Its normal form is (lambda (a) ((ind-Nat n (λ (m) (-> Atom Atom)) (λ (a) 'foo) (λ (n-1 result_n-1 a) 'bar))) a). It's considered simpler and more direct because it's not neutral, instead it's a value, I would guess. $\endgroup$
    – CrabMan
    Sep 4 at 22:19
  • 1
    $\begingroup$ If e is a type and G is an expression which is a type whenever e is a type, and f is a variable of type (Pi ((x e)) G), why is (lambda (x) ((lambda (y) (f y)) x)) not the normal form of (lambda (y) (f y))? Because (lambda (y) (f y)) is not a neutral expression. $\endgroup$
    – CrabMan
    Sep 4 at 22:28
  • $\begingroup$ Why can a neutral expression of one of the types Nat, A+B ,U be normal? I would guess that it can be normal because those three types have multiple constructors, so if the expression is neutral, then we don't know which constructor was used. But can a neutral expression of the type Atom be normal? $\endgroup$
    – CrabMan
    Sep 4 at 22:35
  • $\begingroup$ If I write (the (-> (-> Atom Atom) (-> Atom Atom)) (λ (f) f)) in Pie, it outputs (the (→ (→ Atom Atom) Atom Atom) (λ (f x₁) (f x₁))). I think this means that the type Atom should also be added to your list of three special types. $\endgroup$
    – CrabMan
    Sep 4 at 22:51
  • $\begingroup$ @CrabMan Quite. I forgot there is an Atom type. It is actually special because it is not defined by a universal property (i.e. it doesn't have an eliminator). So the definition of normal/neutral can bend a bit. For example you can consider an atom to be neutral. It doesn't break the theory. $\endgroup$
    – Trebor
    Sep 5 at 3:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.