Generalising KnowNat/Char/Symbol?

[Oleg Grenrus]

I think this is libraries at haskell.org issue.

Most non-beginners have used KnownSymbol or KnownNat, GHC.TypeLits was
meant to be "internal" module but now it's the module everyone uses.

To me abstracting KnownValue like that seems to be reinventing Sing(I)
from singletons:
-
https://hackage.haskell.org/package/singletons-3.0/docs/Data-Singletons.html#t:SingI
-
https://hackage.haskell.org/package/singletons-base-3.0/docs/src/GHC.TypeLits.Singletons.Internal.html#SNat
  ((re)defines separate GADTs for SNat and SSymbol)

- Oleg

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