Right way to specialize structures?

Stream: new members

[Quang Dao]

I want to define the general syntax of a cryptographic commitment scheme:

structure CommitmentScheme where
  Data : Type
  Randomness : Type
  Commitment : Type
  commit : Data → Randomness → Commitment

I also want to define specialized versions of commitment schemes, for instance where Data := List Datum for some type Datum, or where Randomness := Empty. I can't just define something like:

structure ListCommitmentScheme extends CommitmentScheme where
  Data := List Datum

since it gives no guarantee that Data is always List Datum, only that List Datum is the default option for Data.

One way I thought of is to add a proof of equality:

structure ListCommitmentScheme extends CommitmentScheme where
  Datum : Type
  hData : Data = List Datum

This seems clunky to me, since I have to keep casting (hData ▸ x) for any x : List Datum. Is there a better way to do this?

[Kyle Miller]

This is a reason to use type parameters, for example

structure CommitmentScheme (Data : Type) (Randomness : Type) (Commitment : Type) where
  commit : Data → Randomness → Commitment

structure ListCommitmentScheme (Datum : Type) (Randomness : Type) (Commitment : Type)
    extends CommitmentScheme (List Datum) Randomness Commitment

[Kyle Miller]

It seems that it's usually better to have all your types be parameters unless you have a really good reason not to.

[Notification Bot]

Quang Dao has marked this topic as resolved.

[Kyle Miller]

You can always use sigma types to package them up with the types in the occasional context where you need to.

[Notification Bot]

Quang Dao has marked this topic as unresolved.

[Quang Dao]

Is there a way out if I don't want to pass in many type parameters? For instance, if I bundle them up via a structure:

structure CommitmentSpec where
  Data : Type
  Randomness : Type
  Commitment : Type

then is there a reasonable definition of ListCommitmentSpec that extends CommitmentSpec?

[Kyle Miller]

I think the only options really are the hData field or promoting a field to a parameter.

[Quang Dao]

I suppose another way is to define ListCommitmentSpec (resp. ...Scheme) separately, then define a Coe instance to CommitmentSpec (resp. ...Scheme). This way I only need to state defs/theorems about CommitmentScheme once, and they also apply to ListCommitmentScheme via coercion.

Keeping this thread open in case people find problems with my proposal, or have other thoughts.

[Kyle Miller]

That makes sense too, though an issue you might find is the fact that the types of terms have different phrasings, like if s : ListCommitmentSpec and x : List s.Datum then you also have x : (s : CommitmentSpec).Data. They're defeq, but it could cause issues for things that match on syntax (typeclasses, simp, etc.)