4 ms·

> I often wish I worked in a language where I could start dynamic and end statically... I can imagine writing the core of an algorithm and then gradually tighte

> I often wish I worked in a language where I could start dynamic and end statically... I can imagine writing the core of an algorithm and then gradually tightening the conditions as it comes into focus. More than a tool, this would be a practice: progressive type elaboration. Bingo. I love this idea. I haven't tried it yet myself, but I think mypy [1] from Dropbox makes this a reality today in the Python world. [1]: http://mypy-lang.org/ http://mypy-lang.org/

tylerjwilk00 9y ago
I know it's not a favorite lang around here but this is exactly what modern php is.
- kod 9y ago
  How exactly does modern php (not Hack or another vm) let you "start dynamic and end statically"? declare(strict_types=1); is checking and throwing type errors at runtime, not compile time.
ACow_Adonis 9y ago
I believe it's called Common Lisp, specifically SBCL :) Live the dream :P
sitkack 9y ago
Came here to mention MyPy and optional typing, the preferable term Gradual Typing means something distinctly different. http://mypy-lang.org/about.html http://mypy-lang.org/about.html Dropbox employs the creator of MyPy but it isn't a creation of dropbox. Type Systems as Macros http://www.ccs.neu.edu/home/stchang/pubs/ckg-popl2017.pdf http://www.ccs.neu.edu/home/stchang/pubs/ckg-popl2017.pdf Pluggable Type Systems http://bracha.org/pluggableTypesPosition.pdf http://bracha.org/pluggableTypesPosition.pdf Propositions as Types http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-... https://www.youtube.com/watch?v=IOiZatlZtGU https://www.youtube.com/watch?v=IOiZatlZtGU
- tedmiston 9y ago
  > Came here to mention MyPy and optional typing, the preferable term Gradual Typing means something distinctly different. Are you sure that gradual typing is different than what Mypy supports? The Wikipedia page for gradual typing cites mypy as an example. https://en.wikipedia.org/wiki/Gradual_typing https://en.wikipedia.org/wiki/Gradual_typing The Mypy docstrings specifically state: > Mypy has a powerful type system with features such as type inference, gradual typing, generics and union types. https://github.com/python/mypy/blob/272d0c4c50918a36b57e7c0cc85c8cc6306ca72c/setup.py#L34 https://github.com/python/mypy/blob/272d0c4c50918a36b57e7c0c... The section on gradual typing in PEP 483 seems consistent with this as well. https://www.python.org/dev/peps/pep-0483/#summary-of-gradual-typing https://www.python.org/dev/peps/pep-0483/#summary-of-gradual...
  - sitkack 9y ago
    Do they really insert extra dynamic checks? Is Sound Gradual Typing Dead? https://news.ycombinator.com/item?id=11041272 https://news.ycombinator.com/item?id=11041272 http://prl.ccs.neu.edu/gtp/research.html http://prl.ccs.neu.edu/gtp/research.html It was my understanding that MyPy was purely compile time with no runtime checks. But I could be wrong. Gradual Typing as implemented in the original paper would lead to much much slower code. The weight of a static language bolted onto a dynamic runtime for the worst of both possible worlds. Sufficiently abstract Python code is almost un-typable. I think eventually we will get there, where one can explore a program in a dynamic language and ship a correctly statically typed one. Types are only the beginning.
    - tedmiston 9y ago
      I believe you're right that Mypy only offers compile time type checking, but not runtime. It looks like there are some active projects for runtime type checking in Python and while I don't believe Mypy is related to any of them, enforce [1] looks to also use the same standard type hinting syntax from PEP 484. [1]: https://github.com/RussBaz/enforce https://github.com/RussBaz/enforce
newen 9y ago
That's how I write in Julia. Start with an algorithm with no types and eventually introduce type contraints everywhere, and even adding new types.
mercer 9y ago
General question for those more experienced than I am with statically typed languages: would Clojure's 'spec' or Elixir's 'dialyzer', or perhaps TypeScript, fit the bill? If not, what's the downside between these what appear to me 'gradually typed' languages/approaches? To provide some context: my first experience with static (or rather explicit?) typing was TypeScript, and I really liked what I saw.

tylerjwilk00 9y ago

I know it's not a favorite lang around here but this is exactly what modern php is.

kod 9y ago
How exactly does modern php (not Hack or another vm) let you "start dynamic and end statically"? declare(strict_types=1); is checking and throwing type errors at runtime, not compile time.

ACow_Adonis 9y ago

I believe it's called Common Lisp, specifically SBCL :) Live the dream :P

sitkack 9y ago

Came here to mention MyPy and optional typing, the preferable term Gradual Typing means something distinctly different. http://mypy-lang.org/about.html http://mypy-lang.org/about.html Dropbox employs the creator of MyPy but it isn't a creation of dropbox. Type Systems as Macros http://www.ccs.neu.edu/home/stchang/pubs/ckg-popl2017.pdf http://www.ccs.neu.edu/home/stchang/pubs/ckg-popl2017.pdf Pluggable Type Systems http://bracha.org/pluggableTypesPosition.pdf http://bracha.org/pluggableTypesPosition.pdf Propositions as Types http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-... https://www.youtube.com/watch?v=IOiZatlZtGU https://www.youtube.com/watch?v=IOiZatlZtGU

tedmiston 9y ago
> Came here to mention MyPy and optional typing, the preferable term Gradual Typing means something distinctly different. Are you sure that gradual typing is different than what Mypy supports? The Wikipedia page for gradual typing cites mypy as an example. https://en.wikipedia.org/wiki/Gradual_typing https://en.wikipedia.org/wiki/Gradual_typing The Mypy docstrings specifically state: > Mypy has a powerful type system with features such as type inference, gradual typing, generics and union types. https://github.com/python/mypy/blob/272d0c4c50918a36b57e7c0cc85c8cc6306ca72c/setup.py#L34 https://github.com/python/mypy/blob/272d0c4c50918a36b57e7c0c... The section on gradual typing in PEP 483 seems consistent with this as well. https://www.python.org/dev/peps/pep-0483/#summary-of-gradual-typing https://www.python.org/dev/peps/pep-0483/#summary-of-gradual...
- sitkack 9y ago
  Do they really insert extra dynamic checks? Is Sound Gradual Typing Dead? https://news.ycombinator.com/item?id=11041272 https://news.ycombinator.com/item?id=11041272 http://prl.ccs.neu.edu/gtp/research.html http://prl.ccs.neu.edu/gtp/research.html It was my understanding that MyPy was purely compile time with no runtime checks. But I could be wrong. Gradual Typing as implemented in the original paper would lead to much much slower code. The weight of a static language bolted onto a dynamic runtime for the worst of both possible worlds. Sufficiently abstract Python code is almost un-typable. I think eventually we will get there, where one can explore a program in a dynamic language and ship a correctly statically typed one. Types are only the beginning.
  - tedmiston 9y ago
    I believe you're right that Mypy only offers compile time type checking, but not runtime. It looks like there are some active projects for runtime type checking in Python and while I don't believe Mypy is related to any of them, enforce [1] looks to also use the same standard type hinting syntax from PEP 484. [1]: https://github.com/RussBaz/enforce https://github.com/RussBaz/enforce

newen 9y ago

That's how I write in Julia. Start with an algorithm with no types and eventually introduce type contraints everywhere, and even adding new types.

mercer 9y ago

General question for those more experienced than I am with statically typed languages: would Clojure's 'spec' or Elixir's 'dialyzer', or perhaps TypeScript, fit the bill? If not, what's the downside between these what appear to me 'gradually typed' languages/approaches? To provide some context: my first experience with static (or rather explicit?) typing was TypeScript, and I really liked what I saw.