Saturday 6 September 2008

cycle = concat . repeat = fix . (++)

It's annoying that I don't know how to write this totally point free.

(1)
concat . repeat
 { repeat = fix . (:) }
concat . fix . (:)
 { eta }
\x -> (concat . fix . (:)) x
 { compute }
\x -> concat (fix ((:) x))
 { f (fix g) = fix h <= f . g = h . f }
 { concat . ((:) x) = ((++) x) . concat } <- (2)
\x -> fix ((++) x)
 { eta }
fix . (++)

(2)
concat . ((:) x)
 { concat = foldr (++) [] }
foldr (++) [] . ((:) x)
 { eta }
\xs -> (foldr (++) [] . ((:) x)) xs
 { compute }
\xs -> foldr (++) [] (x:xs)
 { compute }
\xs -> x ++ (foldr (++) [] xs)
 { eta }
((++) x) . foldr (++) []
 { concat = foldr (++) [] }
((++) x) . concat

5 comments:

M. Todd said...

What... what is this written with? I have no idea what it mean. I believe I recognize Haskell, but that syntax blows my mind and I don't even know what's going on there.

Tristram said...

They are proofs not programs. The parts in curly brackets are justifications for each step in the proof.

BMeph said...

Except, it fails for [].

Whoops... ;)

nornagon said...

fix . (++) *is* point-free. Even though the standard definition of the Y combinator in Haskell is explicitly recursive, there are ways to fool the type system into allowing a truly point-free Y combinator.

Anonymous said...

nornagon:

bits like:

\xs -> (foldr (++) [] . ((:) x)) xs

aren't point free.