To throw out additional related work, I had a need for runtime values that
capture type-level naturals. It’s used primarily for representing the widths
in a type-safe bitvector formulas.
The code is a few years old, but publicly available here:
https://github.com/GaloisInc/parameterized-uti
Oh, yes---`sameNat` is indeed quite similar to my `compareEv`. I hadn't
noticed. Thanks, Simon.
On Thu, May 24, 2018 at 2:30 PM, Simon Peyton Jones
wrote:
> I see this in GHC.TypeNats
>
> *sameNat ::* *(KnownNat a, KnownNat b) =>*
>
> * Proxy a -> Proxy b -> Maybe (a :~: b)*
>
> *sameN
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
inde
I'm glad to know. Thanks for the endorsement, Richard.
On Thu, May 24, 2018 at 1:05 PM, Richard Eisenberg
wrote:
> Just to add my 2 cents: I've played in this playground and used the same
> structures as David. I second his suggestions.
>
> Richard
>
>
> On May 24, 2018, at 3:54 PM, Conal Elliot
Just to add my 2 cents: I've played in this playground and used the same
structures as David. I second his suggestions.
Richard
> On May 24, 2018, at 3:54 PM, Conal Elliott wrote:
>
> Great! Thanks for the suggestion to use type equality and coerced `Refl`. -
> Conal
>
> On Thu, May 24, 201
Great! Thanks for the suggestion to use type equality and coerced `Refl`.
- Conal
On Thu, May 24, 2018 at 10:43 AM, David Feuer wrote:
> On Thu, May 24, 2018, 1:03 PM Conal Elliott wrote:
>
>> Thanks for this suggestion, David. It seems to work out well, though I
>> haven't tried running yet.
>
On Thu, May 24, 2018, 1:03 PM Conal Elliott wrote:
> Thanks for this suggestion, David. It seems to work out well, though I
> haven't tried running yet.
>
> > unsafeDict :: Dict c
> > unsafeDict = unsafeCoerce (Dict @ ())
> >
> > unsafeSatisfy :: forall c a. (c => a) -> a
> > unsafeSatisfy z | Di
where `Dict` is from Ed Kmett's constraints library (
https://hackage.haskell.org/package/constraints).
On Thu, May 24, 2018 at 10:03 AM, Conal Elliott wrote:
> Thanks for this suggestion, David. It seems to work out well, though I
> haven't tried running yet.
>
> > unsafeDict :: Dict c
> > unsa
Thanks for this suggestion, David. It seems to work out well, though I
haven't tried running yet.
> unsafeDict :: Dict c
> unsafeDict = unsafeCoerce (Dict @ ())
>
> unsafeSatisfy :: forall c a. (c => a) -> a
> unsafeSatisfy z | Dict <- unsafeDict @ c = z
Now we can define `compareEv`:
> compareE
