Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

TypeEqualsBool class can assert type inequality. #29

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

matthewleon
Copy link
Contributor

@matthewleon matthewleon commented Jan 26, 2018

Depends on Instance Chains.

This moves the type equality test here from purescript-type-equality, which would be deprecated if this proposal were to be accepted. I don't really see a way to do this otherwise, as type-level Boolean is defined in this lib.

This is inspired by some chats on Slack, as well as the example @LiamGoodacre made for Instance Chains: https://github.com/purescript/purescript/blob/master/examples/passing/InstanceChain.purs

@garyb garyb changed the base branch from master to compiler/0.12 May 22, 2018 16:01
@thomashoneyman thomashoneyman changed the base branch from compiler/0.12 to master January 20, 2021 05:20
@JordanMartinez
Copy link
Contributor

This PR adds a type class TypeEqualsBool that is essentially a type-level function that determines whether two types are equal or not. Conceptually, it's the below value-level code but at the type level

class TypeEqualsBool :: forall k1 k2. k1 -> k2 -> Bool -> Constraint
class TypeEqualsBool a b (o :: Boolean) | a b -> o

instance reflTypeEqualsBool :: TypeEqualsBool a a True
else instance notTypeEqualsBool :: TypeEqualsBool a b False

This library also attempts to port over the TypeEquals class defined in the purescript-type-equality library. We could keep TypeEqualsBool here, or we could merge it in the purescript-type-equality library. Thoughts?

@thomashoneyman
Copy link
Member

I don't believe we have to merge type-equality into this library anymore in order to implement this, because we no longer have the kind Boolean definition in this library post-polykinds -- but I might be mistaken. If I am mistaken, then it's not possible to merge this into type-equality and if we want this then type-equality will have to be folded into this library.

@JordanMartinez
Copy link
Contributor

AFAICT, [Boolean]https://pursuit.purescript.org/builtins/docs/Prim#t:Boolean) is a kind that is defined in Prim, whose values are defined in [Prim.Boolean]((https://pursuit.purescript.org/builtins/docs/Prim.Boolean).

Thinking about this more, I don't think type-equality should be folded into this library because it's often used in one-off situations that aren't type-level-related per se. However, TypeEqualsBool is clearly a type-level construct. So, I think merging it here makes sense.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants