[Haskell-cafe] Re: instance Eq (a -> b)
ashley at semantic.org
Thu Apr 15 04:12:40 EDT 2010
On Thu, 2010-04-15 at 03:53 -0400, roconnor at 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
> 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
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
More information about the Haskell-Cafe