Opened 5 years ago

Closed 5 years ago

#10082 closed bug (invalid)

Church Booleans - xor

Reported by: honza889 Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.9
Keywords: Cc: honza889@…
Operating System: Linux Architecture: x86_64 (amd64)
Type of failure: Incorrect result at runtime Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by honza889)

When I use following implementation of Church Booleans, all is ok:

lTrue = \x y -> x
lFalse = \x y -> y
lNot = \t -> t lFalse lTrue
lXor = \u v -> u (lNot v) (lNot lNot v)
lXor' = \u v -> u (v lFalse lTrue) (v lTrue lFalse)

But this simplified versions of lXor fails, if first parameter is lFalse:

lXor'' = \u v -> u (lNot v) (v)  -- not work, bug in ghc?
lXor''' = \u v -> u (lNot v) v  -- not work, bug in ghc?
GHCi, version 7.10.0.20150123: http://www.haskell.org/ghc/  :? for help
Prelude> :l lambda.hs 
[1 of 1] Compiling Main             ( lambda.hs, interpreted )
Ok, modules loaded: Main.
*Main> (lXor'' lFalse lFalse) 1 0

<interactive>:3:1:
    Non type-variable argument in the constraint: Num (t5 -> t4 -> t5)
    (Use FlexibleContexts to permit this)
    When checking that it has the inferred type
      it :: forall t4 t5. Num (t5 -> t4 -> t5) => t5 -> t4 -> t5

<interactive>:3:24:
    Could not deduce (Num (t20 -> t30 -> t30))
      arising from the literal 1
    from the context (Num (t5 -> t4 -> t5))
      bound by the inferred type of
               it :: Num (t5 -> t4 -> t5) => t5 -> t4 -> t5
      at <interactive>:3:1-26
    The type variables t20, t30 are ambiguous
    In the third argument of lXor'', namely 1
    In the expression: (lXor'' lFalse lFalse) 1 0
    In an equation for it: it = (lXor'' lFalse lFalse) 1 0

Because both lXor implementations in first example works ok and simplified implementation should be equivalent, I believe this is bug in ghc. But similar problem occure also in older versions of ghc:

GHCi, version 7.6.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> :l lambda.hs 
[1 of 1] Compiling Main             ( lambda.hs, interpreted )
Ok, modules loaded: Main.
*Main> (lXor'' lFalse lFalse) 1 0

<interactive>:3:24:
    No instance for (Num (t20 -> t30 -> t30))
      arising from the literal `1'
    Possible fix:
      add an instance declaration for (Num (t20 -> t30 -> t30))
    In the third argument of lXor'', namely `1'
    In the expression: (lXor'' lFalse lFalse) 1 0
    In an equation for `it': it = (lXor'' lFalse lFalse) 1 0

<interactive>:3:26:
    No instance for (Num (t50 -> t40 -> t50))
      arising from the literal `0'
    Possible fix:
      add an instance declaration for (Num (t50 -> t40 -> t50))
    In the fourth argument of lXor'', namely `0'
    In the expression: (lXor'' lFalse lFalse) 1 0
    In an equation for `it': it = (lXor'' lFalse lFalse) 1 0

Change History (3)

comment:1 Changed 5 years ago by honza889

Cc: honza889@… added

comment:2 Changed 5 years ago by honza889

Description: modified (diff)

comment:3 Changed 5 years ago by simonpj

Resolution: invalid
Status: newclosed

You are trying to use higher rank types here, so you need type signatures. (See Practical type inference for higher rank types). This works:

{-# LANGUAGE RankNTypes #-}
module T10082 where

type CBool = forall a. a->a->a
lTrue :: CBool
lTrue = \x y -> x

lFalse :: CBool
lFalse = \x y -> y

lNot :: CBool -> CBool
lNot = \t -> t lFalse lTrue

lXor :: CBool -> CBool -> CBool
lXor = \u v -> u (lNot v) (lNot (lNot v))  -- You omitted some parens here!

lXor' :: CBool -> CBool -> CBool
lXor' = \u v -> u (v lFalse lTrue) (v lTrue lFalse)

lXor'' :: CBool -> CBool -> CBool
lXor'' = \u v -> u (lNot v) (v)  

lXor''' :: CBool -> CBool -> CBool
lXor''' = \u v -> u (lNot v) v 

So it all seems fine to me. I'll close as invalid but do re-open if you disagree.

Simon

Note: See TracTickets for help on using tickets.