dfeuer
  • Member for 7 years, 11 months
  • Last seen more than a month ago
accepted
comment

@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.

comment

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.

comment

@user65526, sorry, I'm half asleep. What I meant was HList : [Type] -> Type.

comment

Another dependent approach is HList : (ts : [Type]) -> Type, a type parameterized by a list of the types of each of its elements.

comment

@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.

revised

added 79 characters in body

Loading…
revised

edited body

Loading…
asked
Loading…
awarded
comment

@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.

answered
Loading…
awarded
revised

added 233 characters in body

Loading…
revised

edited body

Loading…
asked
Loading…
comment

Perhaps the forall is for parameters and the pi for indices?

awarded
revised

added 124 characters in body

Loading…
asked
Loading…