Mind this program:
{-# LANGUAGE RankNTypes #-}
import Prelude hiding (sum)
type List h = forall t . (h -> t -> t) -> t -> t
sum_ :: (Num a) => List a -> a
sum_ = \ list -> list (+) 0
toList :: [a] -> List a
toList = \ list cons nil -> foldr cons nil list
sum :: (Num a) => [a] -> a
-- sum = sum_ . toList -- does not work
sum = \ a -> sum_ (toList a) -- works
main = print (sum [1,2,3])
Both definitions of sum are identical up to equational reasoning. Yet, compiling the second definition of works, but the first one doesn't, with this error:
tmpdel.hs:17:14:
Couldn't match type ‘(a -> t0 -> t0) -> t0 -> t0’
with ‘forall t. (a -> t -> t) -> t -> t’
Expected type: [a] -> List a
Actual type: [a] -> (a -> t0 -> t0) -> t0 -> t0
Relevant bindings include sum :: [a] -> a (bound at tmpdel.hs:17:1)
In the second argument of ‘(.)’, namely ‘toList’
In the expression: sum_ . toList
It seems that RankNTypes
breaks equational reasoning. Is there any way to have church-encoded lists in Haskell without breaking it??
I have the impression that ghc percolates all for-alls as left as possible:
and
can be used interchangeably as witnessed by:
Which could explain why
sum
's type cannot be checked. You can avoid this sort of issues by packaging your polymorphic definition in anewtype
wrapper to avoid such hoisting (that paragraph does not appear in newer versions of the doc hence my using the conditional earlier).