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