#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