Is it possible to create an alias for a higher kind type?

[chirsz-ever]

Thanks for The Little Typer and this interesting language!
I want to write something about Leibniz Equality in Pie, so I define it as this:

(claim L-≡ (Π ((A U)) (→ A A U)))
(define L-≡
  (λ (A x y)
    (Π ((P (→ A U))) (Pair (→ (P x) (P y)) (→ (P y) (P x))))))

But it causes an error: "U is a type, but it does not have a type.".
After thinking, I found that it is because (Π ((P (→ A U))) (Pair (→ (P x) (P y)) (→ (P y) (P x)))))) is not a U, for (→ A U) is not a U.
Although the above can't be compiled, the Leibniz Equality could be expressed in Pie. We need a "partial definition":

(claim L-≡p (Π ((A U)) (→ A A (→ A U) U)))
(define L-≡p
  (λ (A x y P)
    (Pair (→ (P x) (P y)) (→ (P y) (P x)))))

Then we have to write (Π ((P (→ A U))) (L-≡p A x y P)) wherever we want to express the "real" (L-≡ A x y).
Is there a way to define L-≡ directly, or is it possible to add some macro syntax in Pie?

[xieyuheng]

Maybe we can add "U is U" mode to pie (like agda's "type in type" mode).

[david-christiansen]

Pie itself doesn't have a way to do what you want to do.

I suggest that you take this opportunity to fork Pie and add the necessary feature! In earlier stages of development, Pie had a cumulative hierarchy of universes. This means two things:

1. U is parameterized by a level number, so U becomes (U 0), and it has type (U 1), which has type (U 2) and so on. These are not Nats per se, they just look like them.
2. The type equivalence check becomes a subtyping check. That is, instead of A and B are the same type you get A is a subtype of B. The rules for this look like:

n < k
------------------
(U n) <: (U k)

For base types, they just look like sameness:

------------
Nat <: Nat

For types with parameters, most follow their arguments, so:

E1 <: E2
------------------------
(List E1) <: (List E2)

and so forth.

For Pi, the argument type goes the other way:

A2 <: A1
x : A2 |- B1 <: B2
------------------------------------
(Pi ((x A1)) B1) <: (Pi ((x A2)) B2)

These together are enough to get an ergonomic system with much more expressive power than Pie has. We had these rules in Pie, but we discovered that the book and all the homework we assigned for a class based on it and all the students' answers never used more than (U 0), so we dropped the feature to make the implementation and the language both simpler.

Another good alternative is to go over to Idris, Lean, Agda, or Coq, all of which have many more features but are based on similar ideas to Pie.

In any case, I'm not going to add it to this repository, because this repository should match what's in The Little Typer. I hope that the appendix in the book and the code in the repository are self-explanatory enough to enable you to understand how it works - if not, please let me know!