Last active
August 18, 2018 18:27
-
-
Save KingoftheHomeless/1216debb87a5d44e173977dfb6bb6187 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import Data.List.NonEmpty | |
--These are the definitions I'll use in my proof: | |
fmap :: (a -> b) -> NonEmpty a -> NonEmpty b | |
fmap f (a :| as) = f a :| Prelude.fmap f as | |
extract :: NonEmpty a -> a | |
extract (a :| _) = a | |
duplicate :: NonEmpty a -> NonEmpty (NonEmpty a) | |
duplicate l@(_ :| as) = l :| go_dupe as | |
where | |
go_dupe (x:xs) = (x :| xs) : go_dupe xs | |
go_dupe _ = [] | |
-- zipped = zipWith id | |
zipped :: NonEmpty (a -> b) -> NonEmpty a -> NonEmpty b | |
zipped (f :| fs) (a :| as) = f a :| go_zipped fs as | |
where | |
go_zipped (f' : fs') (a' : as') = f' a' : go_zipped fs' as' | |
go_zipped _ _ = [] | |
{- | |
(<@>) = zipped | |
is a valid ComonadApply instance for NonEmpty. | |
PROOF: | |
Associativity for `zipWith id` is already known. | |
extract (ff <@> fa) === extract ff $ extract fa | |
extract (ff <@> fa) | |
-- let ff = (f :| fs) | |
-- let fa = (a :| as) | |
-- definition of (<@>) | |
=== extract (f a :| go_zipped fs as) | |
-- definition of extract | |
=== f a | |
extract f $ extract a | |
-- let ff = (f :| fs) | |
-- let fa = (a :| as) | |
=== extract (f :| fs) $ extract (a :| as) | |
-- definition of extract | |
=== f $ a | |
=== f a | |
duplicate (f <@> a) === (<@>) <$> duplicate ff <@> duplicate fa | |
duplicate (ff <@> fa) | |
-- let ff = (f :| fs) | |
-- let fa = (a :| as) | |
-- definition of (<@>) | |
=== duplicate (f a :| go_zipped fs as) | |
-- definition of duplicate | |
=== (ff <@> fa) :| go_dupe (go_zipped fs as) | |
(<@>) <$> duplicate ff $ duplicate fa | |
-- (<$>) = fmap | |
=== (fmap (<@>) (duplicate ff)) <@> duplicate fa | |
-- let ff = (f :| fs) | |
-- definition of duplicate | |
=== (fmap (<@>) (ff :| go_dupe fs)) <@> duplicate fa | |
-- definition of fmap | |
=== ((ff <@>) :| fmap (<@>) (go_dupe fs)) <@> duplicate fa | |
-- let fa = (a :| as) | |
-- definition of duplicate | |
=== ((ff <@>) :| fmap (<@>) (go_dupe fs)) <@> (fa :| go_dupe as) | |
-- definition of (<@>) | |
=== (ff <@> fa) :| go_zipped (fmap (<@>) (go_dupe fs)) (go_dupe as) | |
For: | |
duplicate (f <@> a) === (<@>) <$> duplicate ff <@> duplicate fa | |
to be proven equal, we must show that: | |
go_dupe (go_zipped fs as) === go_zipped (fmap (<@>) (go_dupe fs)) (go_dupe as) | |
Proof by induction: | |
Base case: | |
fs and/or as is [] | |
go_dupe (go_zipped fs as) | |
-- definition of go_zipped: | |
-- go_zipped [] as === go_zipped fs [] === [] | |
=== go_dupe [] | |
-- definition of go_dupe | |
=== [] | |
go_zipped (fmap (<@>) (go_dupe fs)) (go_dupe as) | |
If fs === []: | |
go_zipped (fmap (<@>) (go_dupe [])) (go_dupe as) | |
-- definition of go_dupe | |
=== go_zipped (fmap (<@>) []) (go_dupe as) | |
-- definition of fmap | |
=== go_zipped [] (go_dupe as) | |
-- definition of go_zipped | |
=== [] | |
If as === []: | |
go_zipped (fmap (<@>) (go_dupe fs)) (go_dupe []) | |
-- definition of go_dupe | |
=== go_zipped (fmap (<@>) (go_dupe fs)) [] | |
-- definition of go_zipped | |
=== [] | |
we have: | |
go_dupe (go_zipped fs as) === go_zipped (fmap (<@>) (go_dupe fs)) (go_dupe as) | |
Induction step: | |
let fs = (f' : fs') | |
let as = (a' : as') | |
And assume: | |
go_dupe (go_zipped fs' as') === go_zipped (fmap (<@>) (go_dupe fs')) (go_dupe as') | |
go_dupe (go_zipped fs as) | |
-- definition of go_zipped | |
=== go_dupe (f' a' : go_zipped fs' as') | |
-- definition of go_dupe | |
=== (f' a' :| go_zipped fs' as') : go_dupe (go_zipped fs' as') | |
go_zipped (fmap (<@>) (go_dupe fs)) (go_dupe as) | |
-- definition of go_dupe | |
=== go_zipped (fmap (<@>) ((f' :| fs') : go_dupe fs')) ((a' :| as') : go_dupe as') | |
-- definition of fmap | |
=== go_zipped (((f' :| fs') <@>) : fmap (<@>) (go_dupe fs')) ((a' :| as') : go_dupe as') | |
-- definition of go_zipped | |
=== ((f' :| fs') <@> (a' :| as')) : go_zipped (fmap (<@>) (go_dupe fs')) (go_dupe as') | |
-- definition of (<@>) | |
=== (f' a' :| go_zipped fs' as') : go_zipped (fmap (<@>) (go_dupe fs')) (go_dupe as') | |
per our assumption, | |
go_dupe (go_zipped fs' as') === go_zipped (fmap (<@>) (go_dupe fs')) (go_dupe as') | |
we have: | |
go_dupe (go_zipped fs as) === go_zipped (fmap (<@>) (go_dupe fs)) (go_dupe as) | |
Thus, | |
go_dupe (go_zipped fs as) === go_zipped (fmap (<@>) (go_dupe fs)) (go_dupe as) | |
Thus, | |
duplicate (f <@> a) === (<@>) <$> duplicate ff <@> duplicate fa | |
-} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment