#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]:
The H.M algorithm is based on the reasoning of the Modus Ponens.\\
Yes: type inference is monotonic. That is, adding more definitions cannot make previously correct code become incorrect. (For example importing a compiled module and adding definitions in this module cannot invalidate the type inference in the imported module.) (That's not quite true in GHC with some of the 'advanced' extensions; and that's why type inference can become incoherent.)
The inference algorithm tells us which type has a value, but it does not tell us what type does not have the value.
(Not sure I understand but ...) that's impossible in general: there might be a later definition, perhaps in another module, that will provide a suitable type.
The utility of Modus tollens is complementary for many checks.
Please give some examples of the checks you're talking about. This is all very abstract so far.
I also propose that an inference algorithm based on Modus Tollens be coded in GHC.
Coded where? You mean in a Library/as an operator? Or I think you are talking about type inference in general? Then you would need a very strong reason to overturn Hindley-Milner. I suggest you ask some questions on the cafe; especially to discuss examples. And far-reaching proposals should be submitted through the github process, rather than Trac. There is already one proposal to use [https://github.com/AntC2/ghc- proposals/blob/instance-apartness-guards/proposals/0000-instance- apartness-guards.rst 'negative information' in type inference] -- kinda. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13038#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler