Add a total order on type constructors

[guest]

Several proposals for ExtensibleRecords can be implemented as libraries if type constructors can be ordered globally.

This proposal is to add built-in types:

data LabelLT
data LabelEQ
data LabelGT
type family LabelCMP

such that, for any two datatypes

data N = N
data M = M

the instance LabelCMP N M takes one of the values LabelLT, LabelEQ, LabelGT depending on the lexicographic ordering on the fully-qualified names of N and M.

[sorear]

I hate this proposal, but something like it is dearly needed, and I don't want to see yet another bikeshed war. Adding myself to the CC.

[claus]

the ticket neglects to mention that at least one of the record libraries under discussion does not need such an ordering.

that does not imply that the feature might not be useful, and most of the record libraries do indeed employ such an ordering. but, as any other form of reflection, it would have to be designed very carefully: one usually cannot avoid destroying at least some program equivalences when introducing reflection, so at the very least, one needs to be able to separate programs that use such feature (where those equivalences will fail) from programs that do not (where reasoning about programs is not affected).

examples of equivalences no longer valid under this proposal are renaming types or modules and moving types or modules in the module hierarchy.

perhaps type-level ordering should only be available for members of a type class, such as the existing Data or Typeable? and perhaps it should be based on random uniqueIds, similar to Data.Typeable.typeRepKey? but that has its own issues..

@GHC-HQ: how do i add myself to the cc without voting in favour? should there be two cc-lists?-)

[guest]

The problem with using uniqIds is that the order used when a module is compiled must be the same as the order used when it is imported. Do the existing uniqIds have that property?

The suggestion to restrict this to a special type-class is a good one. Maybe this should be done as a special kind of deriving. I would prefer a new class to an extension of an existing one.

[sorear]

Replying to guest:

The suggestion to restrict this to a special type-class is a good one. Maybe this should be done as a special kind of deriving. I would prefer a new class to an extension of an existing one.

There is always Oleg's TTypeable (which Data.Derive can handle); otoh, it uses fundeps.

Chakravarty: Is it feasable to make fundeps and type families 'compatible' in the sense that either can depend on the other?

[nfrisby]

Summary: I think type-level digits/numerals and a type-level reflection of the globally unique-name as a type-level numeral would subsume the proposed functionality.

(This ticket seems quite stale — has there been any more decisions regarding this?)

If the ordering can be arbitrary, I think type-level serializations fit the bill. I chose to "serialize" the types as their global names, so the order of compilation shouldn't matter — everything is based on GUIDs. (I don't think this address Reinke's program logic concerns.)

For the details, see my Hackage packages type-cereal, type-ord, and type-ord-spine-cereal which rely on type-spine and type-digits.

• type-digits declares a fixed set of type-level digits (* -> *, terminated with ()) and means to build numerals from them
• type-ord declares LabelCMP (as Compare) with instances for each pair of those digits and ((), ())
• type-cereal declares a type family Serialize and a (TH) function for representing bytestrings as type-level numerals (to hijack the cereal package's serialization)
• type-spine declares a type-level "spine-view"
• type-ord-spine-cereal declares "generic" LabelCMP instances using the spine-view to reduce all (spine-view-enabled) types to applications of serializable names and then uses the type-digits' LabelCMP instances and a "lexicographic" instance for type-level applications

[morabbin]

Bump; how does this fare given the last five years of type system extensions? (Still ref'd in ExtensibleRecords.)

[goldfire]

As far as I can see, the evolution of the type system hasn't fundamentally changed this issue. With closed kinds (i.e., those from a promoted datatype), it is easy to define an ordering using a type family. But, that doesn't solve the problem for kind *.

There is a chance that any applications that want this feature can use nfrisby's packages, or the upcoming TypeLits? work, which includes type-level strings.

Is there anyone out there who still needs this? What's your application?