jonsterling / agda-calf Goto Github PK

Abstract cost metrics don't really correspond to a notion of "stepping". Would it make sense to rename step to reflect this abstraction? (RaML uses tick, but it suffers from the same issue.) Some ideas:

• spend
• pay
• charge
• incur

(To be read: "X c cost, then run e", for verb X = spend, pay, charge, incur, ...)

So far, we have .agda files. However, it might be worth using Literate Agda files .lagda.md, which lets us:

• include prose describing our constructions, in Markdown (allowing for bold, math, links, etc.)
• default-hide boring details

Only use it to import base types from Agda anyway. On #35, this process is started by adding positive meta⁺; in a follow-up PR, we should remove the existing negative meta and rename meta⁺ to meta.

_&_ is an unusual name for the operation that runs two computations in parallel. It could be confusing, too, since & is often used for "lazy/projective" (negative) product.

Some potential alternatives:

• par, a la 210
• _∥_ (\|| or \parallel in agda-mode)
• _⊗_ (\otimes or \ox in agda-mode)

My instinct is _∥_.

Right now, there are lots of conventions for type names. We should just choose one and stick to it. Proposal:

• type variables:
  • A, B, C for positive types
  • X, Y, Z for negative types
• concrete types:
  • A is an Agda type, e.g. _×_
  • A⁺ is the positive calf type (if applicable), e.g. _×⁺_
  • A⁻ is the negative calf type (if applicable), e.g. _×⁻_