Hi John,
Den søn. 30. dec. 2018 kl. 23.39 skrev John Clements
<cleme...@brinckerhoff.org>:
> 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.
You've actually run into a subtle problem, the solution to which is
not particularly simple!
> 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.
In particular, the rec-Nat case works because the types involved don't
need to be described by U, they just need to be types:
tgt ⇒ Nat base ⇒ t step ⇐ (→ Nat t t)
------------------------------------------
(rec-Nat tgt base step) ⇒ t
> 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.
You're right. You can use rec-Nat in Pie to write things that you
can't write with ind-Nat, precisely because not all types are
described by U. Nicely caught!
> 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?
You're running into some of the limits that we put on Pie to try to
keep it small and simple. There's a few ways that the language could
change to support what you're trying to do:
1. We could add in a predicative hierarchy of universes. This would
mean that U would be U0, and there'd also be U1, U2, U3, etc, such
that Un : Un+1. Then, we could either require you to repeat
definitions at each level, or we could have a rule called
cumulativity, stating:
e : Un
----------
e : Un+1
We actually had this in an earlier version of Pie, but it made the
source code of the type checker significantly more subtle to
understand because the type equality check has to become a type
subsumption check, and subtyping is difficult.
2. Instead of having this rule:
tgt ⇒ (Either A B) mot ⇐ (→ (Either A B) U)
l ⇐ (Π ((a A)) (mot (left a)))
r ⇐ (Π ((b B)) (mot (right b)))
-------------------------------------------------
(ind-Either tgt mot l r) ⇒ (mot tgt)
we could have had this rule:
Γ ⊢ tgt ⇒ (Either A B) Γ, e : (Either A B) ⊢ mot type
Γ ⊢ l ⇐ (Π ((a A)) (mot (left a)))
Γ ⊢ r ⇐ (Π ((b B)) (mot (right b)))
-------------------------------------------------
Γ ⊢ (ind-Either tgt ((e) mot) l r) ⇒ [tgt/e] mot
that makes the motive into an expression with some free variable e. In
other words, the eliminator becomes a binding form that binds a
variable in the motive, rather than using lambda as the ultimate
variable binder. Note that this uses the _is a type_ form of judgment
for the motive, rather than checking that it has the type U. This
would allow also types not described by U to be used.
3. We could give up predicativity, and have U : U. This would leave
the language inconsistent as a logic, however, and allow the encoding
of infinite loops.
In your particular case, you can write a family not inhabited for n=0
or 1 this way:
#lang pie
(claim Two-Or-More
(→ Nat U))
(define Two-Or-More
(λ (n)
(which-Nat n
Absurd
(λ (n-1)
(which-Nat n-1
Absurd
(λ (_)
Trivial))))))
(claim test1 (Two-Or-More 3))
(define test1 sole)
(claim test2 (Two-Or-More 2))
(define test2 sole)
;; These don't type check:
;; (claim test3 (Two-Or-More 1))
;; (define test3 sole)
;; (claim test4 (Two-Or-More 0))
;; (define test4 sole)
You can also round-trip through a sum type with a non-dependent
eliminator. For instance, you could have converted your (Either
Trivial Trivial) to a Nat that is 0 for left, and 1 for right, then
used which-Nat. But that's ugly, and we certainly don't want to end up
Gödel-coding everything!
The real solution is to "graduate" to something like Cur, Idris, Agda,
Coq, or Lean, or alternatively to build a fancier Pie if you prefer to
stay relatively small.
> Thanks in advance!
Thank you for reading it so carefully, and for asking such penetrating
questions!
David
--
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.
