Opened 12 years ago

Last modified 4 years ago

#1894 new feature request

Add a total order on type constructors

Reported by: guest Owned by:
Priority: lowest Milestone:
Component: Compiler (Type checker) Version: 6.8.1
Keywords: Cc: b.hilken@…, sorear
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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.

Change History (24)

comment:1 Changed 12 years ago by guest

Cc: b.hilken@… added

comment:2 Changed 12 years ago by sorear

Cc: sorear added
difficulty: Unknown

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.

comment:3 Changed 12 years ago by 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?-)

comment:4 Changed 12 years ago by 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.

comment:5 in reply to:  4 Changed 12 years ago by 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?

comment:6 Changed 12 years ago by igloo

Milestone: 6.10 branch

comment:7 Changed 11 years ago by simonmar

Architecture: MultipleUnknown/Multiple

comment:8 Changed 11 years ago by simonmar

Operating System: MultipleUnknown/Multiple

comment:9 Changed 10 years ago by igloo

Milestone: 6.10 branch6.12 branch

comment:10 Changed 9 years ago by igloo

Milestone: 6.12 branch6.12.3

comment:11 Changed 9 years ago by igloo

Milestone: 6.12.36.14.1
Priority: normallow

comment:12 Changed 9 years ago by igloo

Milestone: 7.0.17.0.2

comment:13 Changed 9 years ago by igloo

Milestone: 7.0.27.2.1

comment:14 Changed 8 years ago by igloo

Milestone: 7.2.17.4.1

comment:15 Changed 8 years ago by nfrisby

Type of failure: None/Unknown

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

comment:16 Changed 8 years ago by igloo

Milestone: 7.4.17.6.1
Priority: lowlowest

comment:17 Changed 7 years ago by igloo

Milestone: 7.6.17.6.2

comment:18 Changed 7 years ago by morabbin

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

comment:19 Changed 7 years ago by 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?

comment:20 Changed 5 years ago by thoughtpolice

Milestone: 7.6.27.10.1

Moving to 7.10.1.

comment:21 Changed 5 years ago by thoughtpolice

Milestone: 7.10.17.12.1

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:22 Changed 5 years ago by thoughtpolice

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:23 Changed 4 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:24 Changed 4 years ago by thomie

Milestone: 8.0.1
Note: See TracTickets for help on using tickets.