@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
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
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 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) :/
We can reify type equality using a thing like:
if we want to prove that two types are not equal, does it make any sense to reify it as:
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 theNothing
case, you're actually lacking some evidence. specifically you're lacking the evidence thats
is not equal tos'
, 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 symbolhm, but then can you use
sameSymbol
somehow to produceEither (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 classI 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 forunsafeCoerce
in theNothing
case ofsameSymbol
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"at least for the builtin
Symbol
sanother thing that springs to mind is ditching
(~)
and usingCmpSymbol
instead in yourEquals
andNotEquals
, but then you lose the convenience that(~)
provides and you probably need tounsafeCoerce
to recover itI don't have too much experience manipulating
Symbol
s 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 (
Integer
s) :/in any case, if it's okay with you, do share what you ended up using, I'm interested
https://www.stackage.org/haddock/lts-15.8/singletons-2.6/Data-Singletons-Decide.html#t:Decision
singletons gives you a
Decision (a :~: b)
i've never really figured out how to use that evidence