Open Questions

Containers

The standard formulation of containers are structures like [list] that have the signature:

list : Type -> Type

This works great when there is no requirement on the type argument but does not work for structures that require any properties on the element. Perhaps this is only an issue for sets which require a notion of element comparison in order to detect duplication.

Other Languages

Haskell solves this problem by omitting constraints from types.

Proposals

1. Haskell Solution Omitting the relation from the type enables us to state the type class with the standard container formulation. Some potential problems that might occur:
   • Data structures often have invariants that go along with them. These invariants are often written with respect to the relation parameter. It isn't clear how Haskell deals with this issue when there are multiple instances of, e.g. [Eq nat].
2. Subclassing Solution It may be possible to embed these relations into the classes themselves. This allows us to use the same type as in Haskell with operations that are justified automatically by the instance. This suffers from problems where it is difficult to specify the meaning of the operation.
3. Multiple Parameters Rather than having containers with type Type -> Type containers would be defined as Type and have classes that state what the element type is, e.g.

Class Set_ (S : Type) (E : Type) : Type := ...

where S is the type of sets that carry elements of type E. This has the added benefit that things can be declared sets over particular types, e.g. a custom set type can be written specialized for numbers or strings. These are still containers but are not completely polymorphic in their data type.