VisibilityAndEvaluation

I think that some sort of facility for making things abstract is important. A definition f is abstract if its definition cannot be inspected; this means that f does not evaluate (except for inside a certain limited scope, for instance). This is useful for several reasons:

• Hiding implementations, so that client code cannot depend on implementation details.
• Hiding implementations to ensure that some invariant is preserved. My time complexity library relies on the definition Thunk n a = a being abstract, for instance.
• Controlling the extent to which code gets evaluated during type checking, to make things more efficient.

Note that abstraction is not the same as having quotient types (which do not provide a mechanism for hiding implementations).

Currently Agda provides the keyword abstract for making things abstract. Is this the right way to go?

• Perhaps one would want a more integrated approach, in which abstractness is visible in the types of things.
• Perhaps a single mechanism (abstract) is not an optimal way to support all items on the list above.

Few people seem to be aware of the issues raised above, or the presence of abstract, and some discussion about abstraction would be nice.

/NAD