[Haskell-cafe] Can eta-reduction of (\xs -> augment (flip (flip . foldr) xs)) typecheck?
Viktor Dukhovni
ietf-dane at dukhovni.org
Wed Mar 17 02:21:09 UTC 2021
With both `augment` and `foldr` from GHC.Base:
augment :: (forall b. (a -> b -> b) -> b -> b) -> [a] -> [a]
augment g = g (:)
foldr :: (a -> b -> b) -> b -> [a] -> b
...
The function:
\xs -> augment (g xs) where g xs c z = foldr c z xs
-- pointfree: g == flip (flip . foldr)
typechecks (it is in fact just (++))
λ> let g xs c z = foldr c z xs
λ> :t \xs -> augment (g xs)
\xs -> augment (g xs) :: [a] -> [a] -> [a]
Is it possible to explicitly type annotate some `g'` so that the
function:
(\xs -> (augment . g') xs) :: [a] -> [a] -> [a]
is also just (++). That is, basically `g'` is the same as g, but with
an explicit type signature that makes the type checker accept the
eta-reduced composition? A completely naive attempt, with no
type annotations yields:
λ> let g xs c z = foldr c z xs
λ> :t g
g :: [a] -> (a -> b -> b) -> b -> b
λ> :t (augment . g)
<interactive>:1:2: error:
• Couldn't match type: forall b. (a1 -> b -> b) -> b -> b
with: (a -> b0 -> b0) -> b0 -> b0
Expected: ((a -> b0 -> b0) -> b0 -> b0) -> [a1] -> [a1]
Actual: (forall b. (a1 -> b -> b) -> b -> b) -> [a1] -> [a1]
• In the first argument of ‘(.)’, namely ‘augment’
In the expression: augment . g
I haven't found any variant type signatures for "g" that make this go.
I think this may require impredicative polymorphism, and so can't be
done until perhaps QuickLook lands (don't know whether that'll be
enough).
--
Viktor.
More information about the Haskell-Cafe
mailing list