Explicitly distinguish between regular and higher data types

[sattlerc]

Explicitly distinguish between regular and higher data types

[sattlerc]

So, maybe,

higher data Nat : Set
...
higher data Nat : Set where  -- higher is optional here
  Z : ...

Yes (without the second : Set). Do we foresee the possibility of other data type modes that may potentially be mixed with this? If so, higher could be an annotation, e.g., data [higher, second-order, green]. Alternatively, there's always pragmas.

On a second thought, higher isn't really very specific: e.g. higher order data is such that has a constructor with a functional recursive argument. What about cubical data or homotopy data?

I agree. Since the mode is called --cubical, cubical seems an appropriate tag.

[nad]

I think data should come first, and higher/cubical after, because data is the main concept. I also think that, if possible, we should use the same style as for record (or change the notation used for record):

data Unit : Set where
  cubical
  unit : Unit

data Unit : Set
  cubical

data Unit where
  unit : Unit

Instead of higher or cubical one could perhaps use a more descriptive name which indicates that the type has an hcomp constructor, maybe simply hcomp:

data Unit : Set where
  hcomp
  unit : Unit

Here hcomp is a kind of constructor, and it is listed just before the other constructors, but without a type signature. I'm not a big fan of the name "hcomp", though, because both homogeneous and heterogeneous start with "h". Another option might be homogeneous-composition:

data Unit : Set where
  homogeneous-composition
  unit : Unit

[andreasabel]

We could also have a declaration higher-inductive before the constructors (or maybe anywhere in the list), similar to the record flavors (like no-eta-equality).

I suppose this declaration would be optional for data types that have path constructors, right?

[sattlerc]

We could also have a declaration higher-inductive before the constructors (or maybe anywhere in the list), similar to the record flavors (like no-eta-equality).

I suppose this declaration would be optional for data types that have path constructors, right?

Not sure.

Agda already allows splitting the signature

data Nat : Set

from the specification

data Nat where
  O : Nat
  S : Nat → Nat

And thinking long-term, there are proposals for being able to interleave constructors of a data type with other stuff (for example, constructors of other data types in an inductive-inductive definition, or auxiliary definitions). Moreover, composition for a data type can appear in the signature of its constructors.

In these cases, it may be beneficial to know from the start (i.e., the signature, but at least before constructors) if we are in the higher case or not. For example, in the case of Nat, we could have access to the reduction hcomp <false cofibration> O = O after checking the first constructor because we know we are not in the higher case.

That would mean that path constructors can only be used if "higher" is specified. This may also make it simpler in the implementation to gate cubical code and data for higher data types.

higher-inductive

Data is always inductive, so inductive here feels duplicated.

[andreasabel]

So, maybe,

higher data Nat : Set
...
higher data Nat : Set where  -- higher is optional here
  Z : ...

On a second thought, higher isn't really very specific: e.g. higher order data is such that has a constructor with a functional recursive argument.
What about cubical data or homotopy data?

I mean, only because people are used to the initial (bad) naming of a concept, this isn't a reason to chisel this name into stone. (Thinking of the meaningless words alpha-, beta-, etc. -reduction we are stuck with...)

[AndrasKovacs]

I support this, I have it in cctt for the same reasons that @sattlerc mentioned, where both inductive Nat and higher inductive Nat are supported, with different computation rules.

[andreasabel]

So,

cubical data Nat : Set
...
cubical data Nat where  
  -- Should we make "cubical" optional here?
  -- Would be in line with omitting the type signature, although it is just a keyword that has to be duplicated...
  ...

[sattlerc]

If we use "cubical data" as a keyword like that, I feel we would be forced to repeat it.

I'm not a fan of repetition, so as a separate proposal, maybe the syntax for splitting signature and constructors/fields can be shortened to

data D : Set

D where
  [...]

and

record R : Set

R where
  [...]

But maybe that is not possible with the current parser.

[andreasabel]

maybe the syntax for splitting signature and constructors/fields can be shortened

data if_then_else_ (b : Bool) (t e : Set) : Set
...
if b then t else e where
  tt : if true then t else e ≡ t
  ff : if false then t else e ≡ e

[jespercockx]

maybe the syntax for splitting signature and constructors/fields can be shortened

data if_then_else_ (b : Bool) (t e : Set) : Set
...
if b then t else e where
  tt : if true then t else e ≡ t
  ff : if false then t else e ≡ e

That wouldn't work because you can only have higher constructors that target equalities between elements of the type you are defining, but here the equality is between elements of type Set.

But it does remind me of an old proposal (can't find the issue number right away) to have function definitions in this style, i.e.

if_then_else_ : Bool -> a -> a -> a where
  true t f -> t
  false t f -> f

[andreasabel]

@nad: Using a directive like in records was also my first idea, but @sattlerc had objections in #7053 (comment) . How do you see these?

Does your proposal to require the directive with the data signature solve this?

(Note however, that syntax-wise the directive would fit into the list of declarations following the where of the data definition, in analogy to record directives.)

[sattlerc]

Instead of higher or cubical one could perhaps use a more descriptive name which indicates that the type has an hcomp constructor, maybe simply hcomp:

data Unit : Set where
  hcomp
  unit : Unit

Here hcomp is a kind of constructor, and it is listed just before the other constructors, but without a type signature. I'm not a big fan of the name "hcomp", though, because both homogeneous and heterogeneous start with "h". Another option might be homogeneous-composition:

data Unit : Set where
  homogeneous-composition
  unit : Unit

Note that indexed higher inductive types also need a transport constructor (but I am not sure indexed HITs have been fully implemented yet). Would you suggest a keyword also for that constructor?

data Id : A → A → Set where
  homogeneous-composition
  transport
  refl : (a : A) → Id a a

Then indexed data types without transport would have to be rejected. And it is possible to have non-indexed HITs with transport. I guess that's consistent with my proposal.

[nad]

Then indexed data types without transport would have to be rejected.

Another option is perhaps to insert this automatically for indexed types with path constructors.