<div dir="ltr">It's been a while since I've looked at that stuff, but your suggestion seems reasonable to me.</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Mar 16, 2021 at 11:42 AM Sylvain Henry <<a href="mailto:sylvain@haskus.fr">sylvain@haskus.fr</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi,<br>
<br>
I would like to have a KnownWord constraint to implement a type-safe <br>
efficient sum type. For now [1] I have:<br>
<br>
data V (vs :: [Type]) = Variant !Word Any<br>
<br>
where Word is a tag used as an index in the vs list and Any a value <br>
(unsafeCoerced to the appropriate type).<br>
<br>
Instead I would like to have something like:<br>
<br>
data V (vs :: [Type]) = Variant (forall w. KnownWord w => Proxy w -> <br>
Index w vs)<br>
<br>
Currently if I use KnownNat (instead of the proposed KnownWord), the <br>
code isn't very good because Natural equality is implemented using <br>
`naturalEq` which isn't inlined and we end up with sequences of <br>
comparisons instead of single case-expressions with unboxed literal <br>
alternatives.<br>
<br>
I could probably implement KnownWord and the required stuff (axioms and <br>
whatnot), but then someone will want KnownInt and so on. So would it <br>
instead make sense to generalise the different "Known*" we currently <br>
have with:<br>
<br>
class KnownValue t (v :: t) where valueSing :: SValue t v<br>
<br>
newtype SValue t (v :: t) = SValue t<br>
<br>
litVal :: KnownValue t v => proxy v -> t<br>
<br>
type KnownNat = KnownValue Natural<br>
type KnownChar = KnownValue Char<br>
type KnownSymbol = KnownValue String<br>
type KnownWord = KnownValue Word<br>
<br>
Thoughts?<br>
Sylvain<br>
<br>
[1] <br>
<a href="https://hackage.haskell.org/package/haskus-utils-variant-3.1/docs/Haskus-Utils-Variant.html" rel="noreferrer" target="_blank">https://hackage.haskell.org/package/haskus-utils-variant-3.1/docs/Haskus-Utils-Variant.html</a><br>
<br>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>