Fantasy-land: cannot use laws/functor to test composition property

Created on 21 Sep 2016  路  9Comments  路  Source: fantasyland/fantasy-land

identity使:

const identity使 = t => eq => x => {
    const a = t(x)[map](identity);
    const b = t(x);
    return eq(a, b);
};

composition:

const composition = t => eq => x => {
    const a = t(x)[map](compose(identity)(identity));
    const b = t(x)[map](identity)[map](identity);
    return eq(a, b);
};

Consider a in composition:

a = t(x)[map](compose(identity)(identity))

Assume a proof for compose(identity)(identity) = identity:

a = t(x)[map](identity)

The identity property tells us that t(x)[map](identity) = t(x), so:

a = t(x)

Consider b in composition:

b = t(x)[map](identity)[map](identity)

The identity property tells us that t(x)[map](identity) = t(x), so:

b = t(x)[map](identity)
b = t(x)

I think all we're actually proving is compose(identity)(identity) = identity, which isn't at all what we're hoping to prove. :stuck_out_tongue_winking_eye:

For composition to be useful I think it needs to take f :: b -> c and g :: a -> b as arguments.

bug

All 9 comments

Re: statement before 馃嵀

Tbh: i wonder if we should track all the law issues in one issue. I bet there are quite a few.

Tbh: i wonder if we should track all the law issues in one issue. I bet there are quite a few.

Perhaps. I'm now questioning the value of these modules. Since in many cases we need to provide a value (e.g. Just('abc')) or a recipe for constructing a value (e.g. apply Maybe.of to 'abc'), _and_ a function specialized to the outer type (e.g. Maybe) and/or the inner type (e.g. String), we achieve very little code reuse by using functions provided by fantasy-land/laws.

FWIW, composition doesn't really need to be proved:

I wonder, should the spec should even mention it as a requirement?

@joneshf it would be nice if you create an issue for that 馃嵀

composition doesn't really need to be proved

Are you sure this applies in case of JS? Consider this "functor" created from Promise:

Promise.prototype.map = function(f) { return this.then(f) }
const promise = Promise.resolve(1)

// always true, because it's impossible to create promise of promise
promise.map(x => x) === promise

const g = x => Promise.of(x)
const f = promise => promise.map(x => x)

// right hand side will blow up
promise.map(x => f(g(x))) === promise.map(g).map(f)

So if we remove second law, this incorrect functor will become technically correct.

I don't have much want for it to be removed. So, if it's worse, then no change :).

But honestly, you can do similar hacks in haskell with Data.Typeable. That doesn't mean we need to stop believing the proof to be true. If a data type doesn't respect parametricity, I don't know that we should care about that data type.

I mean, the data type's map procedure could look at the current timestamp and throw an exception only when it is congruent to 0 mod 123456789. You'd almost never see it blow up in practice, so both laws would pass, effectively, all of the time. Did the second law help us catch the problem?

I wish we had a law that enforces parametricity somehow :)

I think Fantasy Land is often used by beginners who only start to learn FP, so it would be cool if only by obeying the laws they would fall into pit of success, even if they don't understand why certain law exists.

I'm to be honest one of those beginners :)

TIL: Parametricity also makes any function t :: (Functor f, Functor g) => f a -> g a natural transformation. In other words just by looking at signature we get t(v.map(f)) == t(v).map(f) for free. https://youtu.be/2LJC-XD5Ffo?t=31m22s

Was this page helpful?
0 / 5 - 0 ratings