I see this in GHC.TypeNats
sameNat :: (KnownNat a, KnownNat b) =>
Proxy a -> Proxy b -> Maybe (a :~: b)
sameNat x y
| natVal x == natVal y = Just (unsafeCoerce Refl)
| otherwise = Nothing
The unsafeCoerce says that sameNat is part of the trusted code base. And
indeed, it’s only because SNat is a private newtype (i.e its data constructor
is private to GHC.TypeNats) that you can’t bogusly say (SNat 7 :: SNat 8)
You want exactly the same thing, but for a comparison oriented data CompareEv,
rather than its equality counterpart :~:. So the same approach seems
legitimate.
I always want code with unsafeCoerce to be clear about (a) why it’s necessary
and (b) why it’s sound.
Simon
From: Glasgow-haskell-users <[email protected]> On
Behalf Of Conal Elliott
Sent: 24 May 2018 00:39
To: [email protected]
Subject: Natural number comparisons with evidence
When programming with GHC's type-level natural numbers and `KnownNat`
constraints, how can one construct *evidence* of the result of comparisons to
be used in further computations? For instance, we might define a type for
augmenting the results of `compare` with evidence:
> data CompareEv u v
> = (u < v) => CompareLT
> | (u ~ v) => CompareEQ
> | (u > v) => CompareGT
Then I'd like to define a comparison operation (to be used with
`AllowAmbiguousTypes` and `TypeApplications`, alternatively taking proxy
arguments):
> compareEv :: (KnownNat m, KnownNat n) => CompareEv u v
With `compareEv`, we can bring evidence into scope in `case` expressions.
I don't know how to implement `compareEv`. The following attempt fails to
type-check, since `compare` doesn't produce evidence (which is the motivation
for `compareEv` over `compare`):
> compareEv = case natVal (Proxy @ u) `compare` natVal (Proxy @ v) of
> LT -> CompareLT
> EQ -> CompareEQ
> GT -> CompareGT
Can `compareEv` be implemented in GHC Haskell? Is there already an
implementation of something similar? Any other advice?
Thanks, -- Conal
_______________________________________________
Glasgow-haskell-users mailing list
[email protected]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
