[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 vanto):

 The H.M algorithm is based on the reasoning of the Modus Ponens.\\

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

 The inference algorithm tells us which type has a value, but it does
 not tell us what type does not have the value.
 I also think it is important for the compiler to know what types the
 value does not have.
 To know this, we must infer the inverse of the algorithm and must use
 the Modus Tollens.\\

 {{{
 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
 }}}
 The utility of Modus tollens is complementary for many checks.
 I also propose that an inference algorithm based on Modus Tollens be
 coded in GHC.

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