Is it possible to use church encodings without breaking equational reasoning?

Question

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??

Dionnadionne

Yes, but it will involve hacking on a compiler... rank-2 type inference is decidable, but nobody's implemented it. Rank-3 type inference is undecidable (hence the existence of both Rank2Types and RankNTypes, even though they currently do the same thing). – Moffitt

It's very hard for me to understand what you mean by "equational reasoning" here. You're working with an isomorphism that is quite clearly not the usual equality. – Adlare

@Adlare I'm not sure I know what equational reasoning means, then. I assumed it meant you are free to always inline definitions / beta reduce functions. – Dionnadionne

Ah, I think I misunderstood what you were doing. Sorry. – Adlare

It is okay, I don't know too. – Dionnadionne

@DanielWagner okay then, I guess. :( – Dionnadionne

@Viclib You could of course also use the rank-1 version of the Church encoding, type List r a = (a -> r -> r) -> r -> r, and be careful that you never provide something monomorphic as the first argument of List. It is sad that you can't get the compiler to help you check that, but is also a lot less work. – Moffitt

Well, that is what I was using before, but then how you write head? I tried and it couldn't typecheck for good. – Dionnadionne

@Viclib Remember that it's okay to specialize to the left of arrows. So I would guess head :: List (Maybe a) a -> Maybe a; head f = f Just Nothing or unsafeHead :: List a a -> a; unsafeHead f = f id undefined. – Moffitt

Note that [a] -> List a is a type that doesn't actually exist in GHC, which makes sum_ . toList just plain ill-typed. – Oilcloth

Answer 1

I have the impression that ghc percolates all for-alls as left as possible:

forall a t. [a] -> (a -> t -> t) -> t -> t)

and

forall a. [a] -> forall t . (h -> t -> t) -> t -> t

can be used interchangeably as witnessed by:

toList' :: forall a t. [a] -> (a -> t -> t) -> t -> t
toList' = toList

toList :: [a] -> List a
toList = toList'

Which could explain why sum's type cannot be checked. You can avoid this sort of issues by packaging your polymorphic definition in a newtype wrapper to avoid such hoisting (that paragraph does not appear in newer versions of the doc hence my using the conditional earlier).

{-# LANGUAGE RankNTypes #-}
import Prelude hiding (sum)

newtype List h = List { runList :: forall t . (h -> t -> t) -> t -> t }

sum_ :: (Num a) => List a -> a
sum_ xs = runList xs (+) 0

toList :: [a] -> List a
toList xs = List $ \ c n -> foldr c n xs

sum :: (Num a) => [a] -> a
sum = sum_ . toList

main = print (sum [1,2,3])

Derouen

This is indeed how you should define List. GHC has a rather second class treatment of rank-n types, and using them without a newtype wrapper is going to hurt. – Affinity

Great answer, I hope yours gets accepted over mine. =D – Moffitt

It should also be noted that newtypes add no overhead. – Euxenite

Answer 2

Here is a somewhat frightening trick you could try. Everywhere you would have a rank-2 type variable, use an empty type instead; and everywhere you would pick an instantiation of the type variable, use unsafeCoerce. Using an empty type ensures (so much as it's possible) that you don't do anything that can observe what should be an unobservable value. Hence:

import Data.Void
import Unsafe.Coerce

type List a = (a -> Void -> Void) -> Void -> Void

toList :: [a] -> List a
toList xs = \cons nil -> foldr cons nil xs

sum_ :: Num a => List a -> a
sum_ xs = unsafeCoerce xs (+) 0

main :: IO ()
main = print (sum_ . toList $ [1,2,3])

You might like to write a slightly safer version of unsafeCoerce, like:

instantiate :: List a -> (a -> r -> r) -> r -> r
instantiate = unsafeCoerce

Then sum_ xs = instantiate xs (+) 0 works just fine as an alternative definition, and you don't run the risk of turning your List a into something TRULY arbitrary.

Moffitt

That again... I think I'll just lose the fear and start adopting unsafeCoerce on my vocabulary. You're creating a monster, sir. – Dionnadionne

@Adlare What do you propose instead? – Moffitt

Dunno. Not that. Sometimes the cure is worse than the disease. I don't really see the problem that needs to be solved here. – Adlare

This isn't really constructive but I love dfeuer's reaction, no less than I expected heh – Dionnadionne

(I still don't understand why Haskellers love the type system so much more than they love equational reasoning... I just tend to think nothing in the world comes before it, not even types.) – Dionnadionne

@Viclib I think you should keep your fear. It might be a good idea to try to prove that unsafeCoerce is actually safe -- perhaps the free theorem for List a (or maybe Void?) will tell you what you need to know. – Moffitt

That's horrible. There are no guarantees about unsafeCoerce in general. Any use outside implementation specific modules should be punished in the harshest possible way. – Affinity

@Affinity I think "the compiler doesn't have inference for Rank2Types yet" is one of the perfectly valid excuses. After all, it means the term is correct. Using unsafeCoerce and providing a separated proof looks as acceptable as it gets. Why not? – Dionnadionne

@Affinity I look forward to your proposal for an improved alternative. – Moffitt

After type checking, my ideal compiler would optimize f :: T -> Void as roughly \_ -> undefined, and g :: T -> () as \_ -> () when a termination checker succeeds (similarly for other single-value types, e.g. a:~:b). Since GHC is not (yet) that smart, I guess unsafeCoerce should work, for now. It looks quite dangerous, though. – Crowe

How does this enable equational reasoning? – Euxenite

@PyRulez The complaint in the question is that sum_ . toList and \a -> sum_ (toList a) do not have the same type (one does not even type-check using the code in the question). With my setup, these two terms do indeed both typecheck and produce the same type. – Moffitt

Answer 3

Generally equational reasoning only holds in the "underlying System F" that Haskell represents. In this case, as others have noted, you're getting tripped up because Haskell moves foralls leftward and automatically applies the proper types at various points. You can fix it by providing cues as to where type application should occur via newtype wrappers. As you've seen you can also manipulate when type application occurs by eta expansion since the Hindley-Milner typing rules are different for let and for lambda: foralls are introduced via the "generalization" rule, by default, at lets (and other, equivalent named bindings) alone.

Codling