<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>I think this is <a class="moz-txt-link-abbreviated" href="mailto:libraries@haskell.org">libraries@haskell.org</a> issue.<br>
<br>
Most non-beginners have used KnownSymbol or KnownNat, GHC.TypeLits
was meant to be "internal" module but now it's the module everyone
uses.<br>
<br>
To me abstracting KnownValue like that seems to be reinventing
Sing(I) from singletons:<br>
-
<a class="moz-txt-link-freetext" href="https://hackage.haskell.org/package/singletons-3.0/docs/Data-Singletons.html#t:SingI">https://hackage.haskell.org/package/singletons-3.0/docs/Data-Singletons.html#t:SingI</a><br>
-
<a class="moz-txt-link-freetext" href="https://hackage.haskell.org/package/singletons-base-3.0/docs/src/GHC.TypeLits.Singletons.Internal.html#SNat">https://hackage.haskell.org/package/singletons-base-3.0/docs/src/GHC.TypeLits.Singletons.Internal.html#SNat</a><br>
((re)defines separate GADTs for SNat and SSymbol)</p>
<p>- Oleg<br>
</p>
<div class="moz-cite-prefix">On 16.3.2021 23.45, Iavor Diatchki
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAGK9nuqSAyK9ASe9HVGjmZidYXiFDb5jQqdsq3Y_Cz8=7++csw@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<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"
moz-do-not-send="true">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" moz-do-not-send="true">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"
moz-do-not-send="true">ghc-devs@haskell.org</a><br>
<a
href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs"
rel="noreferrer" target="_blank" moz-do-not-send="true">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
ghc-devs mailing list
<a class="moz-txt-link-abbreviated" href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a>
<a class="moz-txt-link-freetext" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a>
</pre>
</blockquote>
</body>
</html>