2 ms·

Is a type like "fixed-size list of 3 integers" really more useful than a type like "list of integers" plus a constraint "size must be 3"? I feel like the latter

• samus 3mo ago
  To some degree these are the same things, depending on the type system. But it might be easier to write a function accepting a list of size 3 than matching on a constraint, which might get separated from the variable it annotates.
  • inigyou 3mo ago
    The difference is that (generally in programming languages) a type is something defined with a name while a constraint is ad-hoc. If you use types for everything you'll have to write a whole lot: this variable is a Size3List, this one is a Size5List, this one is a PrimePowersList.
• nylonstrung 3mo ago
  > Does Lean have a type for "list containing only prime powers"? You can wrap a base type with a proof which is called bundling inductive PrimePower where | mk (n : Nat) (prf : IsPrimePower n) So in this case the type checker will not allow construction unless the proof demonstrates they are prime powers The prf part gets erased at runtime so there's no overhead. You could also use a constraint/refinement type like you talked about and it's more flexible as it relates to using list operations like map filter reverse etc.