[GHC] #13038: implementation of Modus ponens and Modus tollens

[GHC]

#13038: implementation of Modus ponens and Modus tollens
-------------------------------------+-------------------------------------
        Reporter:  vanto             |                Owner:  (none)
            Type:  feature request   |               Status:  infoneeded
        Priority:  normal            |            Milestone:
       Component:  libraries/base    |              Version:  8.0.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by AntC):

 Replying to [comment:7 vanto]:

 Let me see if I can work an example.

 > 1) f is a function that maps arguments of type A to results of type B.\\
 >
 > {{{
 > f :: A -> B  is identical to v(P -> Q) = 1
 > }}}
 >
 > 2) e is an expression of type A\\
 >
 > {{{
 > e :: A is identical to v(P) = 1
 > }}}
 >
 > 3) Then the application f e has type B\\
 >
 > {{{
 > f e :: B is identical to v(Q) = 1
 > }}}
 >
 > ..., we must infer the inverse of the algorithm and must use
 > the Modus Tollens.\\
 >

 OK let's take the function as `length` from the Prelude.

 {{{
 length :: Foldable t => t a -> Int
 }}}

 And take the use: `if (length xs) then ...`.
 That is, the context tells us to expect result `Bool`,
 which is not `Int`.
 Does this help infer the type for `xs`?

 > {{{
 > 1) f e :: not B is identical to v(Q) = 0
 > }}}
 >
 > {{{
 > 2) f :: A -> B is identical to v(P -> Q) = 1
 > }}}
 >
 > {{{
 > 3) e :: not A is identical to v(P) = 0
 > }}}

 Firstly if this worked, we'd get `xs :: `**not** `(Foldable t => t a)`.
 I'm not seeing how knowing this would help improve the type for `xs`.

 But more importantly this doesn't work.
 If `length`'s result is required to be `Bool` but declared as `Int`, we
 have a contradiction.
 We have both `v(P -> Q) = 1` from the declaration and `v(P -> Q) = 0` from
 the context.

 So GHC should not infer anything about the type for `xs`; it should report
 an error -- which is what it does.

 > The utility of Modus tollens is complementary for many checks.

 No, I think it has no utility.

 > I also propose that an inference algorithm based on Modus Tollens be
 > coded in GHC.
 >

 I propose we close this ticket: invalid.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13038#comment:9>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler