[Haskell-cafe] Re: instance Eq (a -> b)
Ashley Yakeley
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
> 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
More information about the Haskell-Cafe
mailing list