#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:10 vanto]:
Replying to [[span(style=color: #FF0000, AntC )]]:\\ Here is an example.\\
Not needed: I understand how modus tollens works/how to use it. (And you can reasonably expect that anyone who replies to you would know.)
I point out that my idea is to insert the Modus Tollens inside the type inference algorithm ...
Then what is needed is an example of how type inference would work.
Modus Tollens is not specific to programming, it can be found in electronic circuits.(We can build AND,OR,NAND Gates ...)\\
In Boolean logic, we have a closed world: not(True) ==> False; not(False) ==> True. In type inference we don't have a closed world. Knowing that type `a0` is `not(a0 ~ Int)` or `not(Num a0)` doesn't help draw any conclusions about `a0`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13038#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler