On Thu, 2010-04-15 at 03:53 -0400, rocon...@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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
