the-little-typer/pie

Will it be better to elaborate `rec-List` to `ind-List`?

xieyuheng opened this issue · 5 comments

xieyuheng commented

By doing so, we can check that some application of rec-List is equal to some application of ind-List.

(And similar is true for rec-Nat and ind-Nat, and friends...)

david-christiansen commented

There's two reasons that we decided not to do that:

  1. It would mean that users who wrote ind-List in their program might end up with rec-List in an error messages if their motive were not sufficiently dependent. This might be an interesting teaching moment, but we were more worried that it would be frustrating or that users would experience it as a bug.

  2. In Pie, dependent elimination can't compute types. This is because of two design decisions: we have only one universe, and we use functions to express motives. This means that a motive can't be something like (lambda (x) U), because U doesn't have a type in Pie. rec-List doesn't have this limitation, because the type it produces must be a type, but it doesn't need to have a type. This is a fairly subtle point.

xieyuheng commented

Thanks for replying :)

I apologize for opening this kind of issues here.
I learned a lot, but I can imagine it is time consuming for you.

I will post my personal questions in an IRC channel or forum in the future.

brendanzab commented

Perhaps it could help to enable discussions on the pie repo? Then people can continue to see questions, without it being part of the issue tracker, and it being lost in IRC.

david-christiansen commented

The problem with enabling that features is that I'd have to moderate it to keep spam and abuse out, and I don't have a lot of time to be on call for an online forum right now (being a parent to a toddler during a pandemic shortly after an intercontinental move and all that...). I can answer emails, though!

I thought about setting up a mailing list for the book, but I think it's irresponsible to run a discussion forum if one is not in a position to moderate it effectively.

Thanks for the pointer though!

  • 👍1
  • ❤️1
brendanzab commented

Ah yeah, perfectly understandable! And yeah, I know how hard moderation can be. 😔