Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.
We can reify type equality using a thing like:
data Equals a b
Refl :: a ~ b => Equals a b
if we want to prove that two types are not equal, does it make any sense to reify it as:
data NotEquals a b
UnRefl :: (a ~ b => Void) -> NotEquals a b
how do you want to use this?
@Georgi Lyubenov // googleson78 it's a long story. there is a function called sameSymbol :: KnownSymbol s => Proxy s -> Proxy s' -> Maybe (s :~: s'). but in the Nothing case, you're actually lacking some evidence. specifically you're lacking the evidence that s is not equal to s', which can for example be used to demonstrate that e.g. a variant indexed by symbols is phantom in the type parameter corresponding to that symbol
sameSymbol :: KnownSymbol s => Proxy s -> Proxy s' -> Maybe (s :~: s')
hm, but then can you use sameSymbol somehow to produce Either (NotEquals s s') (s :~: s')?
Either (NotEquals s s') (s :~: s')
that's the intent, yes
i don't know that I can use sameSymbol specifically to achieve it, it might require a different class
I would choose some representation that is convenient in your case (either what you proposed or UnRefl :: (s :~: s' -> Void) -> NotEquals s s') and then reach for unsafeCoerce in the Nothing case of sameSymbol
UnRefl :: (s :~: s' -> Void) -> NotEquals s s'
because that's what they do to produce the proof of s :~: s' in the first place, i.e. there is probably no way to produce a proof "legally"
s :~: s'
at least for the builtin Symbols
another thing that springs to mind is ditching (~) and using CmpSymbol instead in your Equals and NotEquals, but then you lose the convenience that (~) provides and you probably need to unsafeCoerce to recover it
I don't have too much experience manipulating Symbols though, so take my words with a grain of salt :)
Yeah, I suppose that makes sense
Ideally I want to avoid getting too symbol-specific, because I need to implement similar things for both nat and symbol indexed kind structures
I wish we could use something like the agda thing where you use a convenient representation for the type checker and proofs (peano naturals) and then it gets compiled using a more performant representation (Integers) :/
in any case, if it's okay with you, do share what you ended up using, I'm interested
singletons gives you a Decision (a :~: b)
Decision (a :~: b)
i've never really figured out how to use that evidence