inference rules do not support *

marcoheisig / restricted-functions

Reasoning about functions with restricted argument types.

MIT License

10 stars 0 forks source link

inference rules do not support * #3

Open guicho271828 opened 5 years ago

guicho271828 commented 5 years ago

Is (integer 0 *) supported in

https://github.com/marcoheisig/restricted-functions/blob/master/code/type-inference-rules/numbers.lisp#L66

guicho271828 commented 5 years ago

CL-USER> (restricted-functions:infer-type nil #'+ '(integer 2 14) '(integer 0 *))
(INTEGER * *)
;; expected (integer 2 *)
CL-USER> (restricted-functions:infer-type nil #'/ '(integer 2 14) '(integer 0 0))
T
;; expected NIL
CL-USER> (restricted-functions:infer-type nil #'/ '(single-float 2.0 14.0) '(single-float 0.0 0.0))
SINGLE-FLOAT
;; expected sb-ext:single-float-positive-infinity or nil or

guicho271828 commented 5 years ago

I would separate the type inference repository from restricted-type

marcoheisig commented 5 years ago

Thank you for the feedback!

The rationale for having (infer-type #'+ '(integer 2 14) '(integer 0 *)) return (integer * *) is that for Petalisp, I only care about upgraded array element types in the end. And I really care about every CPU cycle, so if I can avoid consing, I do so.

But you are right - type inference should be a separate library. Maybe even with a separate API for precise type inference and inference on simplified types.

guicho271828 commented 5 years ago

hmm, for x : (integer 2 14) and y : (integer 0 *), (log (+ x y -3)) would not be able to prove that the result is always real

guicho271828 commented 5 years ago

well, the example is wrong. (log (+ x y)) is just enough. If (+ x y) : (integer 2 *), the result is always a real float. If (+ x y) : (integer * *), (log (+ x y)) : (or (complex ???-float) ???-float) (up to your choice of default float)

My point is, lower bounds are also important. The thing is, in the end it always saves time to make something complete from the beginning.

marcoheisig commented 5 years ago

Hello @guicho271828, great to hear from you!

After some pondering, here is my plan of how to proceed:

For Petalisp, I will use an even weaker, simpler type inference scheme (https://github.com/marcoheisig/Petalisp/blob/master/code/type-codes/type-codes.lisp, if you are interested). The point is I'd rather spend time working on performance and parallelization, than on type inference. And my hope is that this simple scheme will also have fewer, or even zero bugs.
For the general problem of inferring function types, I would probably recommend hooking into SBCL's defoptimizer mechanism, at least for now. In the long run, there should of course be a portable library for that. Maybe I will write that as part of the SICL project. But don't expect anything within the next 1-2 years.

This also means I will probably retract the restricted-functions library from Quicklisp. The good news is that I might instead put my type-codes code on Quicklisp, once it is finished.

guicho271828 commented 5 years ago

by the way, for reference: Upgraded element type in CL implementations https://gist.github.com/guicho271828/a1414527df502eb659e137198bf6764d