Sigma type definition vs definition through constructors

Stream: general

[nrs]

Consider these two definitions of lists of fixed length:

def Vector (α : Type u) (n : ℕ) :=
  { l : List α // l.length = n }

inductive Vect (α : Type u) : Nat → Type u where
   | nil : Vect α 0
   | cons : α → Vect α n → Vect α (n + 1)

And consider these two definitions of Fin

structure Fin (n : Nat) where
  val  : Nat
  isLt : LT.lt val n

inductive Fin' : Nat -> Type
  | zero : Fin' n
  | succ (t : Fin' n) : Fin' (n.succ)

It seems like there is often these two ways of defining a type: either by using a sigma type , i.e. you specify a carrier type and a list of propositions you expect to be satisfied (the first example of each case above), or by directly giving the type in terms of constructors. In both cases above we'd expect the types to be equivalent, but only in the second case there's something like computational content (i.e. you can immediately define a catamorphism with the given definition).

Is there a way to specify rigorously the difference between these two sorts of definitions? Or, is there a way to state, what makes it such that the second sort of definition has computational content but both can be used in proofs?

[Kyle Miller]

What do you mean precisely by only the inductive versions having computational content? The Subtype versions have immediate computational content as well, so long as you are willing to work with List and Nat, respectively, in your folds.

[nrs]

Kyle Miller said:

What do you mean precisely by only the inductive versions having computational content? The Subtype versions have immediate computational content as well, so long as you are willing to work with List and Nat, respectively, in your folds.

It seems to me that in order to work with the subtype versions, you need a partial function, no? I want to say there is noncomputational content because we are not explicitly given which parts of the domain the resulting partial function has values for. By this I mean: the recursor of the inductive versions immediately give a non-partial function defined over the entire domain, while in the case of the subtype definitions, any fold would be a fold over List and Nat where we wouldn't know which values don't belong to said fold unless we provide a proof for the proposition in the subtype definition

[nrs]

(I am not sure this makes sense I am looking to make this more precise)

[Kevin Buzzard]

I don't see any partial functions anywhere. Where are you seeing a partial function? Are you talking about partial?

[Kevin Buzzard]

Vector \a n is a type and you can just consider functions defined on that type.

[Kyle Miller]

Plus, in both Vector and Fin, the properties are Decidable, so there is no mystery about which values can appear.

[Kyle Miller]

You can define the same recursors for Vector and Fin as their Vect and Fin' counterparts (it's a good exercise)

[nrs]

Kyle Miller said:

You can define the same recursors for Vector and Fin as their Vect and Fin' counterparts (it's a good exercise)

hm I will be thinking about this, thank you both for the answers

[nrs]

Kyle Miller said:

Plus, in both Vector and Fin, the properties are Decidable, so there is no mystery about which values can appear.

it does seem however that those cases where a definition like Vect and Fin' is available is also a case where the properties are decidable, and definitions such as Vect and Fin' are not possible otherwise (this is why I referred to maybe there being something about computational content, maybe direct inductive definitions are not possible in those cases where the subtype would contain an undecidable proposition?)

[Kyle Miller]

If the subtype has an undecidable proposition, would it even be possible to cast it as an inductive of the forms you're considering?

[nrs]

Kyle Miller said:

If the subtype has an undecidable proposition, would it even be possible to cast it as an inductive of the forms you're considering?

Right this is what I am saying, it seems to me that maybe not. But how can we formalize the difference between these two types of definitions in such a way to be able to prove this statement?

[Kyle Miller]

I'd guess the reason that there's this formal relationship is that both are of the form { x : T // f x = true } where f is a function defined recursively on T.

[Kyle Miller]

It seems to me that in this case you can encode f into T to make a type T' with an extra Bool index, with those terms where the index is true are valid ones.

[Kyle Miller]

And then you can optimize this index away, at least for Vect and Fin'

[nrs]

Kyle Miller said:

And then you can optimize this index away, at least for Vect and Fin'

Thank you very much for your answers! I will be thinking about these comments