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