[Haskell-cafe] Re: Unique functor instance

[Janis Voigtlaender]

DavidA wrote:
> Okay, I see. Well that's interesting, because it suggests that your proof 
> might break under modest extensions to the language.

Yes. The free theorem used was a "naive" one, for the simplest possible
model of Haskell, not even taking care of possible nontermination and
seq. But http://linux.tcs.inf.tu-dresden.de/~voigt/ft/ can produce less
naive ones as well. In particular, it can also produce free theorems for
types involving class constraints, like Eq or Ord. That would deal with
situations where the type variables a and b in the type of fmap were
class-constrained, as you suggest.

And finally, another plug: explanations for precisely the kind of
type-based reasoning I used in the earlier mail can be found in the
thesis I advertised today on the general list:
http://wwwtcs.inf.tu-dresden.de/~voigt/habil.pdf

Ciao, Janis.

-- 
Dr. Janis Voigtlaender
http://wwwtcs.inf.tu-dresden.de/~voigt/
mailto:voigt at tcs.inf.tu-dresden.de