Multisets

[ivanperez-keera]

I'm interested in representing multisets.

In particular, instead of plain lists, like:

'[A, B, A, C]

or perhaps sets with repeated elements:

Set '[A, B, A, C]

I'm looking for something like:

Set '[ (A, 2), (B, 1), (C, 1) ]

Now, I can achieve something like this with Maps:

Map '[ A :-> Int, B :-> Int, C :-> Int ]

But those Ints would be given a value during runtime. What I want to resolve the values of those Ints during compile time:

Map '[ A :-> 2, B :-> 1, C :-> 1 ]

It tried the obvious way, but it complains that:

    • Expected kind ‘[Mapping Symbol *]’,
        but ‘'[A ':-> 1]’ has kind ‘[Mapping * Nat]’

Any advice?