#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