Canonical types defined as functions into universe (feature request)

cmcmA20 commented 5 days ago

Problem

There's a tension between two desires: to have seamlessly composable code gadgets and to have proper abstraction barriers.

Postulating a new name is a form of human communication, names usually signal that the denoted concepts are important in some way. Specifying computational behaviour of these things is a completely unrelated activity. Currently Agda presents you with three principal options for animating a named thing in a universe:

type is canonical, no values (postulate)
type is canonical, values compute as prescribed by a least/greatest fixpoint of an implicitly defined functor (data / record)
type is not canonical, it computes like a function into universe, values compute accordingly

Transparent functions into universe create unpleasant goals and hide interesting structure in a soup of lower-level primitives. Opaque functions into universe restrict computation for both name and its' values.

Solution

We should also have the ability to create canonical types with values that compute according to a function definition. These canonical type aliases don't explode under reduction in goals and don't force you to have a ton of opaque blocks.

Authors of Narya express this idea as

This sort of "recursively defined canonical type" helps maintain information about the meaning of a type, just like using a custom record type rather than a nested Σ-type; eventually we hope it will be helpful for unification and typeclass inference.

A few examples where it can be useful

Parameterized `data` types

Antimodularity at its finest. Usually we stick to inductive definitions with nice names like List and prove (by pattern matching) a myriad of trivial lemmas about functoriality etc. Compositional framework of polynomial functors or descriptions solves trivial stuff once and for all, but sigma pie is a bit too messy in goals. pattern synonyms are a band-aid, the wound shouldn't be inflicted in the first place.

Subcategories

All kinds of subcategories (vanilla, full, wide) deserve to have distinct names but may also benefit from computing as a total category for some displayed category.

h-levels

Consider 1lab's H-Level definition. Having a wrapper record with a hierarchy of instances duplicating the corresponding theorems is a direct consequence of the current state of affairs. Making is-hlevel opaque would not help as opaque definitions are transparent for instance resolution.

Vectors

Vec : Type ℓ → (n : ℕ) → Type ℓ
Vec _ 0       = ⊤
Vec A (suc n) = A × Vec A n

Reduction to product frequently breaks argument inference and instance resolution , map/fold usability is unnecessarily lacking in comparison to inductive Vec.

Notes on implementation

IIUC constructor type should never be inferred so we don't lose anything when checking constructor against an alias type. If opaque infrastructure can be reused, most (all?) of this feature can also be done with minimal effort inside the elaborator.

UlfNorell commented 2 days ago

Can you give some more fleshed out concrete examples of what you are suggesting. For instance, I don't understand how properties get lifted from the underlying type if all we do in the implementation is changing type checking of constructors.

nad commented 19 hours ago

Making is-hlevel opaque would not help as opaque definitions are transparent for instance resolution.

Some of us discussed something similar in a recent meeting: should opaque definitions be treated as transparent by the positivity checker? I think most agreed that opaque definitions should be opaque. If that is not the case when it comes to instance resolution, then I think we should fix that. I suggest that you open a separate issue for this.

agda / agda