Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

cannot use laws/functor to test composition property #172

Closed
davidchambers opened this issue Sep 21, 2016 · 9 comments
Closed

cannot use laws/functor to test composition property #172

davidchambers opened this issue Sep 21, 2016 · 9 comments
Labels

Comments

@davidchambers
Copy link
Member

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. 😜

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

@SimonRichardson
Copy link
Member

Re: statement before 🍭

@SimonRichardson
Copy link
Member

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

@davidchambers
Copy link
Member Author

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.

@joneshf
Copy link
Member

joneshf commented Sep 21, 2016

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

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

@safareli
Copy link
Member

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

@rpominov
Copy link
Member

rpominov commented Sep 21, 2016

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.

@joneshf
Copy link
Member

joneshf commented Sep 22, 2016

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?

@rpominov
Copy link
Member

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 :)

@rpominov
Copy link
Member

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

5 participants