Generalising KnowNat/Char/Symbol?

16 Mar 2021

      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-Uti...

Sylvain Henry

Iavor Diatchki

Oleg Grenrus

tags

participants (3)