Generalising KnowNat/Char/Symbol?

[Iavor Diatchki]

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> 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
> 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/20210316/4f26a92d/attachment.html>