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

TypeEqualsBool class can assert type inequality. #29

Open matthewleon opened 6 years ago

matthewleon commented 6 years ago

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

JordanMartinez commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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.