Type-level _as_int functions for enumerations?

[martinberger]

Enums come with a mapping to other data types, e.g.

enum E with as_int -> int = {
   A => 1,
   B => 4,
   C => 7
}

The mapping between the symbolic name and the corresponding int is available at compile time, so I should be able to do something like this

type T ('n) = { 'n, <constraints>. int('n) }
type TA = T(E_as_int(A))
type TB = T(E_as_int(B))
...

Is this currently possible? There does not seem to be a type-level E_as_int.

[Alasdair]

It's not currently possible. Would need to think about the syntax in types a bit.

[martinberger]

It's probably only marginally useful and might not be worth compilcating the language. I have a use case in the implementation of Zc* where that would add more type-safety (or more specifically, let me get away without internal_error(...) in pattern matching).

[martinberger]

It's not currently possible. Would need to think about the syntax in types a bit.

PS, just to double-check: this is not even possible with the autogenerated map to numbers if the user simply defines enum {A, B, C}?

[Alasdair]

No, we don't lift enumerations to the type level at all.

[Alasdair]

There's no theoretical reason why we couldn't. It might make Coq generation more complicated with more things at the type level, but enumerations are essentially equivalent to a limited set of numbers.