search

purescript / purescript-typelevel-prelude

Types and kinds for basic type-level programming
BSD 3-Clause "New" or "Revised" License
63 stars 21 forks source link

Add type-level Equals for Boolean #66

Closed JordanMartinez closed 3 years ago

JordanMartinez commented 3 years ago

Fixes #65

hdgarrood commented 3 years ago

I’m wary of adding things before we have a concrete use case for them. Is that the case here?

JordanMartinez commented 3 years ago

I don't have a good case in mind. I believe this would be required if one ever created a type-level list of booleans and wanted to find an element within that list. But I can't think of a scenario where one would want to do that at the type-level.

JordanMartinez commented 3 years ago

@kl0tl Since you originally suggested this, do you have any concrete use cases in mind?

kl0tl commented 3 years ago

I did not propose this class with a specific use case in mind, but I guess it would be needed to implement the characteristic function of a relation that holds either when it does or fails for all its premises (but not when it fails only for some of them). For example with type-level routes you may need this to know if all routes in a set of alternatives are either auth protected or unprotected.

Without some boolean equality we can only express the characteristic function of relations that hold when they do for all (with And) or any (with Or) of their premises. The same line of reasoning would support also adding xor and logical implication.

I’m fine waiting for concrete use cases though, this is easy enough to implement elsewhere if needed in the meantime.

JordanMartinez commented 3 years ago

We could leave this PR open until such a use case emerges and then merge this PR and make a release pretty trivially, right? However, I'm not sure I'd want an open PR on a repo that may never get merged. So, should this actually be closed instead?

hdgarrood commented 3 years ago

I’d rather close this than leaving it open for merging at some unspecified future date, yeah. The PR will still be there if someone looks at the list of closed PRs.