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