On Thu, 2010-04-15 at 03:53 -0400, roconnor@theorem.ca wrote:
Hmm, I guess I'm carrying all this over from the world of dependently typed programming where we have setoids and the like that admit equality relations that are not necessarily decidable. In Haskell only the decidable instances of equality manage to have a Eq instance. The other data types one has an (partial) equivalence relation in mind but it goes unwritten.
But in my dependently typed world we don't have partial values so there are no bottoms to worry about; maybe these ideas don't carry over perfectly.
It's an interesting approach, though, since decided equality seems to capture the idea of "full value" fairly well. I'm currently thinking along the lines of a set V of "Platonic" values, while Haskell names are bound to expressions that attempt to calculate these values. At any given time during the calculation, an expression can be modelled as a subset of V. Initially, it's V, as calculation progresses it may become progressively smaller subsets of V. Saying a calculation is bottom is to make a prediction that cannot in general be decided. It's to say that the calculation will always be V. If it ever becomes not V, it's a "partial value". If it ever becomes a singleton, it's a "complete value". On the other hand, this approach may not help with strict vs. non-strict functions. -- Ashley Yakeley