Why the choice for big-step evaluation rules rather than single-step in your PDF? Just curious.

]]>“ordinary” mean lazy or eager? If you mean eager, I agree that lambdas are values, but cbv lambda translates into thunk lambda, so it remains a value in cbpv. ]]>

The unity of duality paper also had some misleading terminology, and these days I like to speak of both positive and negative values, and positive and negative continuations. My favorite way to think about these is in terms of pattern-matching: positive types are *eliminated* (i.e., we build positive continuations) by pattern-matching, while negative types are introduced (i.e., we build negative values) by pattern-matching. This explains why the ordinary function space of functional programming is negative, because we define functions by pattern-matching. (A positive function space would be weird, because it would be eliminated by pattern-matching…but indeed that’s what the paper on “focusing on binding and computation” is about.) A slightly subtle point, though, is that we build negative values by pattern-matching against patterns of *destructors.* It so happens that a destructor pattern for A -> B contains a constructor pattern for A (and a destructor pattern for B). You can also think of the negative type of lazy pairs: the way we build a lazy pair is by pattern-matching against the two possible destructors, fst and snd, saying what value to return in each case.

I don’t think Conor’s ever written anything up about Frank, but you might be interested in the slides of his talk at the Effects in Type Theory Workshop.

Noam: Thanks for your reply! I’ve had “Read Noam’s Agda code” on my “Todo someday” list for about a year now. I guess I got distracted by writing my thesis

Ralf Hinze was visiting when I gave talked about this and he asked an interesting question: why does the function space necessarily build computation types? I’m afraid I couldn’t give him a satisfactory answer. Do you have a convincing explanation?

Hank: Computation types are what Noam calls “negative types” – types characterised by their elimination rules rather than their introduction rules. For example, the function space operator build computation types. In Paul and Noam’s work, functions abstract over value types but return computation types. Inhabitants of Nat would be values (which is different from a computation that will return a Nat).

]]>Is Nat a value or a computation?

Hank

]]>Thanks! ]]>