[Haskell-cafe] Re: Unique functor instance

Janis Voigtlaender voigt at tcs.inf.tu-dresden.de
Tue Nov 25 10:43:16 EST 2008

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:

Ciao, Janis.

Dr. Janis Voigtlaender
mailto:voigt at tcs.inf.tu-dresden.de

More information about the Haskell-Cafe mailing list