search

josefs / Gradualizer

A Gradual type system for Erlang
MIT License
609 stars 35 forks source link

How to mention Gradualizer in a paper? #565

Closed kikofernandez closed 1 month ago

kikofernandez commented 1 month ago

Hi,

I would like to cite Gradualizer in a paper, and to categorise it correctly (if there is any known way to cite Gradualizer, please let me know)

Having said this, I believe Gradualizer is a soft (optional) type system, in the same sense as eqWAlizer from WhatsApp. In the intro of the repo, there is a link to "gradual typing", and said link mentions:

Allowing the implicit converson from ? to int is unsafe, and is what gives gradual typing the flavor of dynamic typing. Just as with dynamic typing, the argument bound to x will be checked at run-time to make sure it is an integer before the addition is performed.

Essentially, when we go from untyped to typed code, we need to check that the typed code is correct (via a type test), so that we can maintain soundness in the typed parts.

AFAIK, Gradualizer is strictly not a gradual type system based on that definition, or does Gradualizer introduce type tests from untyped to typed code?

Thanks!

erszcz commented 1 month ago

Hi @kikofernandez!

Indeed, you're right - Gradualizer does not inject type tests, so technically speaking it's not a "proper" gradual type system. The ? type, any() in Gradualizer, is just considered compatible with any other type. I imagine the intention was there, but the project never came close enough to realising it.

I don't know if there's "a proper way" to cite it in a paper. The few mentions I know of just point at the GitHub URL.

kikofernandez commented 1 month ago

Thanks for the quick response @erszcz !

I will reference the repo then :)

Thanks a lot!