@user65526, I mention Haskell because it's a language I know well, and so I can express what I want to say in it. It's not actually the best language for expressing these ideas. Computer languages are not just for programming computers; they're for communication.
T : nat -> Type seems like rather stronger medicine than needed for inductive lists.
ts : list Type (or however that's spelled in Coq) should be sufficient. In Haskell, we tend to find it easier in many cases to work with a slight generalization:
data Rec :: [k] -> (k -> Type) -> Type. This lets us talk easily about certain important types like
(forall t. f t -> g t) -> forall ts. Rec ts f -> Rec ts g.
@user65526, sorry, I'm half asleep. What I meant was
HList : [Type] -> Type.
Another dependent approach is
HList : (ts : [Type]) -> Type, a type parameterized by a list of the types of each of its elements.
@MarceloFornet, amortization can be resolved with persistence using lazy evaluation, which is what I'm trying to use here. Some problems are more susceptible to a generalization of lazy evaluation. Stacks can of course be represented very simply as linked lists, but each element then requires its own node, with the indirection and overhead that entails.
added 79 characters in body
@JoachimBreitner, yes, I did. I also used the same approach for the new safe merge utilities, although characterizing their precise performance characteristics is surely too difficult to bother with.
added 233 characters in body
Perhaps the forall is for parameters and the pi for indices?
added 124 characters in body