I think this is librar...@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 <sylv...@haskus.fr > <mailto: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 <mailto: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
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs