4 ms·
Though I will continue to claim that quotient types should belong in the list but aren't - even in Cubical Agda that problem's not really solved! If you don't h
by Smaug123 6y ago
Though I will continue to claim that quotient types should belong in the list but aren't - even in Cubical Agda that problem's not really solved! If you don't have an easily-computed canonical form for your equivalence classes, you're doomed in almost any language.
- valenterry 6y agoThank you for the term "quotient types", that's the first time I'm hearing that!!! I agree that this would be an amazing thing to have, but I've never seen those anywhere in practice (not even in Idris). My gut-feeling tells me that it might not work in combination with composability in the sense that there might never be a proper global "equal" that everyone can agree one. I'm curious - besides the ones mentioned, are there any other fundamental type concepts that you would build into your own programming language? :)
- Smaug123 6y agoSadly I don't have "my own programming language", and even if I did, I think this is an unsolved problem in language design :P Interesting question, though; I'll think about it.