[racket-users] pie: dancing around 'U does not have a type'

['John Clements' via Racket Users]

I’m having a great deal of fun working through The Little Typer. I’ve run into 
a problem that I’m sure has a simple solution, but I don’t know what it is. To 
understand my question, let me first give a simple example.

Here’s a dependent type that’s uninhabited when n is zero:

#lang pie

(claim no-zero-please (-> Nat U))
(define no-zero-please
  (λ (n)
    (rec-Nat n
      Absurd
      (λ (n-1 prev) Trivial))))

(the (no-zero-please 2) sole)
(the (no-zero-please 1) sole)
;;; (no-zero-please 0) is uninhabited

Note the use of rec-Nat, which doesn’t require a motive. What if we use 
ind-Nat, instead? Uh oh:

#lang pie

(claim no-zero-please (-> Nat U))
(define no-zero-please
  (λ (n)
    (ind-Nat n
      ;; this doesn't work:
      (λ (n) U)
      Absurd
      (λ (n-1 prev) Trivial))))

(the (no-zero-please 2) sole)
(the (no-zero-please 1) sole)
;;; (no-zero-please 0) is uninhabited

The problem is that the motive has to have the type (-> Nat U), and U doesn’t 
have type U. The rec-Nat works because no motive is necessary.

This raises the question of whether ind-Nat is strictly more expressive than 
rec-Nat, but in the case of Either, the problem is more severe.

I wanted to try to formulate a type that was uninhabited for n=0 and n=1, and I 
thought I was getting there when I formulated a ternary type and
paired it with a type in a rec-Nat:

#lang pie

(claim discrete-3 U)
(define discrete-3 (Either (Either Trivial Trivial) Trivial))

(claim zogo (-> Nat (Pair discrete-3 U)))
(define zogo
  (λ (n)
    (rec-Nat n
      (the (Pair discrete-3 U) (cons (left (left sole)) Absurd))
      (λ (n-1 prev)
        (ind-Either (car prev)
          ;; oh no! can't type check motive:
          (λ (dc) (Pair discrete-3 U))
          (λ (inner) (ind-Either inner
                       (λ (dc) (Pair discrete-3 U))
                       (λ (dc) (cons (left (right sole)) Absurd))
                       (λ (dc) (cons (right sole) Trivial))))
          (λ (dc) (cons (right sole) Trivial)))))))


The problem is that in this case, AFAICT, there’s no “non-motive” version of 
ind-Either.

Am I missing something obvious?

Thanks in advance!

John





-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.