Airtight vs numpile

[pfalcon]

Thanks for your project! I hope you're aware of https://github.com/sdiehl/numpile which is purposely minimalist example of (simple) type inferencing of Python code. It uses simple equality constraint propagation/solving for type inference. I wonder, if you, based on your experience, can comment whether Hindley-Milner offers any benefits comparing to simple, perhaps adhoc type inferencing approaches? Do Hindley-Milner's complexities and limitations (let's call them such) play anyhow well with Python's rich function semantics (default args, keyword args, etc.) and can be even remotely applied to object-oriented features? Thanks.

[pfalcon]

Really, not insisting on reply here, but just in case a notification of this ticket might be lost in a spur of winter holidays, a friendly ping.

[pfalcon]

It seems that @alehander92 just doesn't watch this project and doesn't receive notifications.

Anyway, to whoever may come here by google, I recently stumbled upon a paper "Generalizing Hindley-Milner Type Inference Algorithms" (e.g. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.18.9348&rep=rep1&type=pdf) which argues:

Type inferencing according to the standard algorithms W and M often yields unin- formative error messages. [...] The method developed here is to first collect constraints from the program, and to solve these afterwards, possibly under the influence of a heuristic. We show the soundness and completeness of our algorithm. The algorithms W and M turn out to be deterministic instances of our method, giving the correctness for W and M with respect to the Hindley-Milner typing rules for free. We also show that our algorithm is more flexible, because it naturally allows the generation of multiple messages.

In other words, they're effectively doing what the Numpile example above does, and argue that it's more flexible approach.

Do Hindley-Milner's complexities and limitations (let's call them such) play anyhow well with Python's rich function semantics (default args, keyword args, etc.) and can be even remotely applied to object-oriented features?

Ocaml turns out to have native support for both keyword and default args, and seems to fair pretty well re: type inference. Well, not much worse than other functional languages, though they mention issues with interaction of default args and currying.

[alehander92]

Oh I missed it somehow sorry

I'll answer tomorrow ,thanks for the links :)

On Thu, Mar 12, 2020, 00:08 Paul Sokolovsky [email protected] wrote:

It seems that @alehander92 https://github.com/alehander92 just doesn't watch this project and doesn't receive notifications.

Anyway, to whoever may come here by google, I recently stumbled upon a paper "Generalizing Hindley-Milner Type Inference Algorithms" (e.g. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.18.9348&rep=rep1&type=pdf) which argues:

Type inferencing according to the standard algorithms W and M often yields unin- formative error messages. [...] The method developed here is to first collect constraints from the program, and to solve these afterwards, possibly under the influence of a heuristic. We show the soundness and completeness of our algorithm. The algorithms W and M turn out to be deterministic instances of our method, giving the correctness for W and M with respect to the Hindley-Milner typing rules for free. We also show that our algorithm is more flexible, because it naturally allows the generation of multiple messages.

In other words, they're effectively doing what the Numpile example above does, and argue that it's more flexible approach.

Do Hindley-Milner's complexities and limitations (let's call them such) play anyhow well with Python's rich function semantics (default args, keyword args, etc.) and can be even remotely applied to object-oriented features?

Ocaml turns out to have native support for both keyword and default args, and seems to fair pretty well re: type inferences. Well, not much worse than other functional languages, though they mention issues with interaction of default args and currying.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/alehander92/Airtight/issues/2#issuecomment-597902078, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAGKZ62T7QCPPIUS7OEV3SLRHADVZANCNFSM4KAI2Q4Q .

[pfalcon]

Thanks for response, if you would have any comments on "Airtight vs numpile" matter, that definitely would be appreciated.

[alehander92]

sorry, i didnt answer these days!

i am sorry, but i cant give a qualified answer: i worked on this project a long time ago, IIRC it doesnt fit too well with python semantics, as i probably expected to use different semantics(basically make a different language). However i'd guess a python-specific approach might be good, after seeing the success of typescript/mypy etc , but if it's about scientific code, not sure

Many people love full type inference, I don't really do full type inference currently anymore, but its so subjective: it seems to me local inference is very nice, but full type inference is often not worth it, if you need to compromise other things for it(and code with signatures seems more readable), note, you can still DRY those signatures somehow

so i cant give you an unbiased opinion!

what are you interested in?

[pfalcon]

what are you interested in?

Well, roughly speaking, I'd be interested in existence of a simple and small enough Python compiler, which would implement a good (sane) subset of semantics, and would easily extendable beyond that. Well, something like that ;-). To that end, I tried to collect retrospective of Python compilers at https://github.com/pfalcon/awesome-python-compilers, and see what would be a good project to continue hack on (I discount big bloated projects like PyPy). Numpile and Airtight caught my attention because both of them have clear type inferencing components.

I don't really do full type inference currently anymore, but its so subjective: it seems to me local inference is very nice, but full type inference is often not worth it, if you need to compromise other things for it(and code with signatures seems more readable)

This argument sounds familiar, I believe I read somewhere. But I understand right that "local type inference" essentially means mandatory annotations on function parameters/returns? I guess such approach wouldn't work for a functional language, where factoring out/creating more functions is a way to do anything. Even for Python it would be a bit said to create a small helper function and be required to annotate it right away...

[pfalcon]

Ocaml turns out to have native support for both keyword and default args, and seems to fair pretty well re: type inference.

This leads to question: what type inference algo Ocaml uses. Quickly google up so far led me to just https://www.cs.cornell.edu/courses/cs3110/2011sp/Lectures/lec26-type-inference/type-inference.htm , which shows an example of type inference implemented in Ocaml using unification algo. Surely, that doesn't mean that production Ocaml compiler uses unification ;-). Guess, would need to look at source to check that...