[Haskell-cafe] Re: instance Eq (a -> b)

[Ashley Yakeley]

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