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

Reply via email to