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 <sylv...@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@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
