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
Subscribe to:
Post Comments (Atom)
5 comments:
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.
They are proofs not programs. The parts in curly brackets are justifications for each step in the proof.
Except, it fails for [].
Whoops... ;)
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.
nornagon:
bits like:
\xs -> (foldr (++) [] . ((:) x)) xs
aren't point free.
Post a Comment