Pyre: Fast Type Checking for Python
facebook.com
facebook.com
After about 10 years of coding in a fit of passion we ended up with huge monolithic projects written in dynamic languages that where extremely brittle.
Fortunately languages with type inference (Rust, Golang, OCaml, Scala, etc) started becoming the answer to our problems. (We also collectively decided that Microservivces were another solution to our woes though that cargo cult is being questioned).
So we have a decade of code and packages written in Python and JavaScript that work well for our use cases (Data Science, MVP web apps/services, Database integration, etc) that is hard to give up. Often because alternatives aren't available yet in the statically typed languages (Hurry up Rust!).
There is often a lot of friction to get new languages introduced. I love Rust, but I don't think I can introduce it into our Golang/NodeJS/Javascript environment anytime soon.
You may be overgeneralizing, depending on whom you mean by the term "we".
More often than not, the code I've written has to be very well trusted when deployed. For me, "getting things done" means getting to effective and trustworthy code ASAP. Static type systems have been invaluable for that work.
However, the grandparent has a point: Java's type system makes static typing much more painful than it needs to be. I didn't start working in Java until fairly recently, and it was only then that I started to understand how many fans of dynamic languages could say that static typing mostly just gets in the way. But, if the only static language you've spent much time with is Java. . . now I get it. Java's type system mostly just gets in the way.
This was actually a replay of what happened with Smalltalk versus C++ in the 80's and 90's, which was a part of the history of how Java came about. And even that was a replay of what happened with COBOL and very early "fourth generation" languages (like MANTIS) from a decade before that!
Writing code is rarely problematic. Usually when you sit down to write code, you have a clear idea of what you want to do. Or if you don't, you have the advantage of being intimately aware of what you're writing.
Once your project becomes large enough that you can't hold it all in your head at once, reading code becomes supremely important.
Any time you write code that interacts with other parts of your project in any way, you will need to understand those other parts in order to ensure you do not introduce errors. That very frequently means being able to read code and understand it correctly.
There's a saying that issues in complex systems always happen at the interfaces.
This is why very terse dynamic languages like Clojure often have relatively low bug counts despite a lack of static checks.
Some interesting reading on this topic:
https://cacm.acm.org/magazines/2017/10/221326-a-large-scale-...
Verbosity hurts reading, not typing. Think of reading an essay that takes hundreds of pages to make an argument that could have been written in a single paragraph.
It absolute is, at least for me. Granted, the majority of time spent during programming is on thinking rather than typing, but any time spent typing detracts from time that could have been spent on thinking instead. Whenever I type a line too long, I tend to lose focus on what I am thinking, and get bogged down by language details. Besides, typing the useless thing again and again (like repeating a long type name) frustrates people, and frustrated people have a harder time to concentrate.
Java never stuck with me because of that, same with trying to learn Objective C. But languages like Swift, Go, Ruby, Python hit the sweet spot.
If you're just using it as a more terse version of Java, then I can understand why you're not seeing much of a change in your experience.
std::vector<std::pair<std::size_t, std::complex<float>>> data = SomeMethod();
auto data = SomeMethod();Rings especially true for my shop as well. I had to introduce Rust or Go, and went with Go. Seeing the mild pushback I get from Go's type system makes me especially glad I didn't choose Rust.
... though, in some cases, Rust+Generics would be easier than Go.
An other possibilities is that Go's static types feel like a lot of ceremony for too little benefit. That was one of my biggest issues with Java, and though Go's lighter it also provides less benefits… By contrast, Rust is in the camp of requiring a higher amount of ceremony but providing a lot of benefits from it (sometimes quipped as "if it compiles it works").
I wouldn't really say that, I think it's more that we all discovered huge monoliths don't work in an "agile cloud" environment where you have 10 teams deploying on their own cadences with no coordination (which you have with on premise binary delivery, or waterfall, or when you have implicit coordination by operations because they have to build out the physical infra). Further, I think modularity has become much bigger in the past 15-20 years as more and more people contribute to open source, more problems become "solved", and languages/domain spaces mature. Whether microservices are the best solution to those observations is still up for debate, but cargo cult or not I doubt many engineers these days would use a magical wand to go back to monoliths even if they live in microservice hell right now.
The performance problems dealing with Tcl on a 2000 startup made me never ever again use programming language without JIT/AOT support for production code.
To this day, Java, .NET and C++ stacks are my daily tools.
You can't even have tuples. Neither tuple-like named types and named records. You have to make class every time, and OOP discipline tells you to hide data in it and make "behavior" public (this approach is definitely not for everything, so "beans" with getters and setters became hugely popular). Ubiquity of hashmaps in dynamic languages is huge relief after that.
Scala has reputation of "rubified java" rather than "FP for java" because of hugely improved expressiveness of types (presence of data types).
The only difference is that you get to eliminate a class of trivial annoyances.
AttributeError: 'NoneType' object has no attribute 'method'
I'm genuinely curious (and probably absurdly naive), but can you explain why you believe that microservice architecture is being questioned, what alternatives there are and why they are better?
That's why you can code in imperative, OO or functional and not just one paradigm.
That's why you can choose between threads, processes and asyncio, or callbacks vs await.
And of course, declaring your types or not.
This allows Python to be suitable for geography, data analysis, scripting, web dev, sysadmin, machine learning, UI, pentesting, etc.
Python is never the best language at anything. But it's a damn good language at most things. It's an invaluable powerful versatile toolbox because it gives you the margin to adopt the style that fits your problem instead of forcing one on you.
It also has the benefit of not getting out of fashion precisely because of that.
I think this so much. What the best programming languages for me isn't necessarily the best at anything, and shouldn't be at all. But it should be 80% of everything the best. And that in itself is possibly even harder to achieve.
I really wish Ruby was the case here. But clearly Python is taking this title.
This is meaningless bullshit. I could say the same thing about Java - tons of battle-tested high-level libraries, and a variety of frontends that all compile onto the same runtime. Just like Python, you can write imperative or functionally, and have your choice of working in a hand-holding high-level framework or down close to the API.
It's a programming language, if it's not a powerful+versatile toolbox it's doing something wrong. Now, if we look at the cases where a programming language is obviously not fit-for-purpose, the common thread is the inability to scale to larger codebases without the programmer effort becoming exponential.
And that's where Python fails, because it's missing a critical piece of the toolbox - type checking. It makes maintaining code vastly more difficult, because you don't have any compile-time checking about how your code is being used. That makes it brittle and difficult to refactor.
> It also has the benefit of not getting out of fashion precisely because of that.
PHP also never goes out of style. Should we all be taking cues for language design from PHP?
I don't think Python is that bad. I write Python code when it's appropriate. But it's not the language I'd choose to write a large, long-lasting codebase in, either.
There's always been more than one way to do things. String formatting, loops/map-filter/comprehensions., Even importing.
The idea is that for whatever you're doing, the language should provide an obvious way to accomplish that. Sometimes that means having competing ways of doing it, so that distinct but similar problems both have obvious solutions.
We are not monks, we live in the real world.
But I also recognize that I work on codebases that live a long time and change and get refactored A LOT. I can't imagine statistical researcher being effective writing effective if he was forced to write his one-off experiments in something like C#, although it's almost the best language for me and my tasks.
And the opposite is true. I'm now working on the first code base so huge that every time i open a file, i annotate all the lines a touch.
That's a beautiful thing.
Python became popular after strong typing was known but before academic research into more advanced systems had entered the mainstream. For many programmers, that experience meant slow compilers, unhelpful error messages requiring ugly syntax to fix, recreating a lot of practical things which were built in to Python, etc. We don’t know how many of them would have preferred something with e.g. Rust-level tooling and capabilities if that had been available.
Our university had quite a few courses where ML was the goto language for project assignments.
In those days Python was hardly used, still trying to get adoption.
By 2000 most Python projects were all about Zope, which I was surprised to find out it is still around.
Anecdotally, I noticed a lot of people who missed some feature from Lisp, C, etc. but generally decided that Python made everything else enough easier that they didn’t mind very much. There’s probably an interesting discussion of language usability in that.
That’s not a slight against the language — they were focused on other goals — but for a long time the conventional wisdom was that it was interesting for CS research and learning but not normal application development whereas you could get quite a lot of work done reasonably in Python at least one decade, probably two, earlier.
I'm sorry to break it to you, but that's an oxymoron. The whole idea of static types is that they don't need to be validated at runtime.
Python has a static type system which is gradual (ie. allows for untyped code) and is separate from the strongly but dynamically typed semantics of Python at runtime. Now, the static type system tries to mirror the dynamic semantics wherever it can, but it's still a completely separate beast. In other words, you don't enforce static types at runtime - you enforce dynamic types at runtime as usual and have an option of additionally using static type system. By the time you run the code, the static types are mostly gone. The fact that the static types reflect the dynamic type system produces an illusion that the static types remain, but they don't.
If what you said was true, the following code would not work:
x: int = 0
x = "0"
print(x)
The Python VM does nothing with the computed type hints. It's only useful for 3rd party tools that want to check the type.s PyCharm does it natively. mypy and pyre are command line tools you can use stand alone or plug into an editor (VSCode integrate very well with mypy).
But that's it.
That's not how it works. Type annotations are ignored at runtime. And to be pedantic, even if they were evaluated at runtime, they would be dynamic types, not static types. :p
The type annotations exist to make the code easier to read and to enable certain kinds of static analysis (including a type checker).
Call it "strongly tagged" if you like, but "type" unqualified should mean static type. Even "dynamic type" is a marketing hijack of the word type.
Professor Robert Harper takes the same position: https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...
When developing, you don't necessarily know about your types yet. And you might not even want to think about them. It's easier to shove in assumptions because things will change as you begin to understand what you want to build as you spend time writing the software.
It's not until later when the code has partially stabilised that you can start spotting what data structures are robust enough to be close to final and actually do benefit from being blessed by typing, locking down the inputs and outputs.
Traditionally, in a dynamically and/or weakly typed language, when the program grows large enough those parts could have been rewritten in a statically and strongly typed language. But if the dynamic language also offers some, even just basic tools for static typing then it all becomes much easier.
This is absolutely not true for myself and my coworkers. We think in types first. Typically we write out high-level functions with type signatures and make sure they all fit together and everything type-checks. Then, we'll fill in the detail and actually implement the functions. Often this process is recursive and we need to repeat it until we get small functions that are either easy to implement or available in a library. We have a type-based search tool to facilitate finding such library functions. Sometimes there are problems and alternative abstractions that only come to light when filling in the details. When a large re-organisation of code is necessary, types again help to get this right.
Personally, I could never build a non-trivial piece of software in a dynamic language. Perhaps I just don't have the brain power to track the types manually in my head.
I don't worry too much about tracking types in my head because with a test and REPL I can quickly and trivially spin up and inspect to the minutest level of detail almost any line of code in a runtime state, use autocomplete, etc. and write reliable snippets of code with a near instantaneous feedback loop - getting instant feedback not just on an object's type and its properties, but on what it actually does when it is run.
Usually when developers used to a statically typed language switch to a dynamically typed language changing their style of development does not occur to them simply because the economics are so different to what they are used to - they rely heavily on IDEs with autocomplete, etc. (which, in statically typed language provides instantaneous feedback) and are used to long compile/test feedback loop and REPLs that are poor to non-existent.
In practice this means a lot of them don't think to go looking for potentially better forms of instantaneous feedback that are more readily available in dynamically typed languages but will kvetch because the one they are used to is suddenly unavailable... ;)
Occasionally, those trivial pieces of software become non-trivial, in which case, having the ability to refactor with type hints is a good thing vs. a complete rewrite in a strongly typed language.
That's the argument I made in "How ignorant am I, and how do I formally specify that in my code?"
http://www.smashcompany.com/technology/how-ignorant-am-i-and...
"2.) the other group of programmers start off saying “There is a great deal that I do not know about this particular problem, and I am unwilling to commit myself to absolute statements of truth, while I’m still groping in the dark.” They proceed with small experiments, they see where they fail, they learn about the problem, they discover the solutions, and they add in type information incrementally, as they feel more confident that they understand the problem and possess a workable solution. These are the dynamic type advocates."
But are you honest with yourself? When working "in the unknown", the basis of your code is nevertheless a set of assumptions. You might not spell them out, but they are there. Static types do not equate pretense of understanding - they are those assumptions made explicit, and more importantly, universal (and not existential like tests). They help reasoning about code (esp with larger codebases/teams) and it is easier to adapt and extend (well, refactor) them in a safe way as the code and with it your knowledge about the problem develops.
Starting with types allows you to play around with data models of the problem space quickly before committing a lot of code to provide a solution. At least that's my take on this.
Now, here's where you usually hear people praise dynamically typed languages—I want to change the design, because I still prototyping. How do I do this? Just change the types (ADTs)!
After changing my design, the compiler will now let me know where my functions don't make sense anymore. Contrast this with when I usually dev in a dynamical language, I end up running my program again at this step, finding out that one function over here didn't like that I'm now passing a string down instead of an Intel, another function was expecting a boolean, but now I'm returning the result instead, etc.
The saying that static languages are not great for prototyping needs to die. They are magnificent, you just need to have a conversation with the compiler instead of fighting it.
Of course, this all assumes a language with a sophisticated enough type system, e.g. Haskell, OCaml, Idris, PureScript, Elm (somewhat), Rust (depending on your do domain), etc.
So often I start out just by banging on something. My domain model isn't well defined, I'm very tolerant of errors, and I really value quick exploration and a fast iteration cycle. If a project starts to mature, though, I start wanting more things that aid long-term maintainability. More type checking. More controlled error handling. More constraints on what code is ok.
Maybe a good example is checked exceptions. Everybody hated those in Java, because it imposed a discipline that's only really valuable in certain situations. In contrast, something like Ruby or Python lets you have a single high-level error handler to start, and gradually tighten things up. Java's type system similarly pushed a lot of people away, because it made them pay up-front costs for down-the-road benefits they might never need. Hopefully this will be a similar thing, where projects big enough to benefit from type discipline will add it as they go.
Type checking is all about complexity management... you don't need it if you're hacking on a weekend project, but when you have hundreds of developers on a million-line codebase, it can save you tons of time.
Dynamic languages have their advantages too (productivity, REPL's, etc.)
Why NOT combine the two features? Just because it's not built into the core of the language doesn't mean you can't benefit from the complexity management aspect if your job is to manage the code complexity in a large developer workforce.
I see this argument a lot but I don't buy it. You might not need Java's SimpleBeanFactoryAwareAspectInstanceFactory but I don't believe putting in types hinders quick prototype development; I think, in general, it helps it. Especially when combined with good tooling and a good IDE.
It especially helps in refactoring things quickly without needing a special IDE environment. It also lets me skip an entire class of unit tests that boil down into type checking.
Quite a few people, myself included, don't use IDEs.
I've seen the productivity argument a lot, so I'm curious about this perspective. What does "productivity" mean here? Shipping code? Because if you ship code that doesn't work, did you really ship it? If you're writing a small throwaway sub-1000-line utility for internal use, I can see that, but if you're getting paid to ship code what is the definition of productivity?
https://docs.microsoft.com/en-us/dotnet/csharp/programming-g...
auto types and lambda functions are the ones that come to my mind. I am sure there are more features making their way into modern C++ versions.
Dynamic typing: C# "dynamic" keyword
Type inference: C# "var" keyword, C++ "auto" keyword
Both of those can be types in a rich enough type system; the latter is a fairly common example for dependent types, for instance.
Have you used this for anything? If so, how was the experience?
I initially thought optional / gradual typing (a la Dart 1) was mad but when you think about it in this context it makes sense. However now Dart 2 has gone back to static typing so who knows...
I've built video streaming websites with a users account, uploads, votes, comments, many filters and hundred of thousand files, holding half a million user a day in Python. The server cost is around a fifth of the generated revenues.
Most projects will never even reach this size, not to mention remotely approaching google size (from 2010).
Something like 10k lines of code or three authors seems to be about the limit where dynamic typing becomes really painful.
It has builtin classes, unlike every other popular language out there.
Every program has to deserialize data like JSON into types and enforce its assumptions about that data whether you have static analysis tooling at compile-time or not.
Hypothesis 2: All successful statically-typed languages eventually grow large enough to have a dynamically typed scripting language embedded in them.
1 - dynamic languages, while granting great freedom, make it easy to shoot yourself in the foot with simple typing bugs, so we cope by adding type checking
2 - many (most?) static type systems are not expressive enough to type some programs, so people embed dynamic solutions to build the stuff they need.
Haskell is pretty decent at typing most stuff I want, but it makes me think about it up front, which is nice sometimes, but not always. Python lets me build stuff quickly and work out the design as I go, but it's hard to make sure everything works as intended. I wish there was something that let me bodge things together, but then constrain them with types when I need to...
(iirc mypy has builtin support for namedtuple, but doesn't really support other types generated at runtime)
Examples are most text editors: emacs (elisp), Sublime Text (Python), Vim (VimScript), Atom (JavaScript). Many games and game engines: World of WarCraft (Lua), Unreal (UnrealScript), SCUMM, etc.
Dynamic codebases are rewritten in static languages to improve maintainability and code quality; programs written in static languages include an interpreter as a feature that supports user-defined programs, e.g., a browser's JS engine or emac's text editor and also for specialty domains where code quality is less important than developer velocity and the static language of choice is unnecessarily painful (games).
Assuming I didn't misrepresent your thesis, does this seem more or less accurate to you?
Lua is of course popular and the topic of using it in games has been done to death: Love2D, Grim Fandango, Don't Starve, Cry Engine, Garry's Mod, etc.
Eve Online supposedly uses Stackless Python and I've seen Vampire the Masquerade Bloodlines (early Source engine) use Python.
Valve's wiki lists Squirrel, Lua, Python and Gamemonkey and they are all dynamic but I think Squirrel is the top language there.
I've also seen Angel Script in HPL1 (the Penumbra series by frictional) but it's another static scripting language and it markets this as a feature.
Unity of course has its C# 'scripts' which are static and I found the idea of scripting in such a behemoth of a language very novel when I've first seen it (yes, UnityScript has dynamic capabilities but it has static ones too and most of the users seem to be with C#).
SCUMM (and Z machine and similar) is a very weird case because it seems more like a script in the sense of a scene play (and the S might stand for script but they were naming utilities after gross stuff like CYST, MMUCUS, etc. so it might be shoehorned), not actual programming language, it's tied to the engine/game/genre/assets way more strongly than even Unreal Script was but I didn't do anything with SCUMM so I can't actually say for sure what would happen if you wrote something that didn't make sense (like tell a table to walk somewhere or reference an object or animation or something else that doesn't exist).
Many Naughty Dog games (including Crash Bandicoot games on PS1 which is frankly insane) also used their own Lisp inspired by Scheme called GOOL and then GOAL but I'm not sure how dynamic it was.
There's also a subtle line between embedding a language to make yourself scriptable and making yourself a library written in mix of C, C++ and that language and there is an interesting article on that[3].
GIMP also includes (or used to?) something related to Scheme/Lisp and has a system in place to support multiple scripting languages at once and calls between any of them called Procedural DataBase. Adobe Lightroom includes Lua too.
Id tech engines apparently used another language/technique each major engine version and I don't know the specifics of it at all.
I'm quite interested in the topic of extending applications (and specifically games) in various scripting languages, plugin systems, etc. but I'd not say all static programs grow dynamic scripting capabilities since AngelScript, Pascal Script (:D), Unreal Script and C# are all static 'scripting' languages and scripting in general is about 'scripting' (as in - small or big bits of code that is easy to change and safe to experiment with modifying a larger program in small or big ways), not necessarily dynamic programming (e.g. you could in theory every viably have Lua scripts in a larger Python program or even AngelScript scripts in a Python program to really mix it up and script a dynamic program with a static scripting language). You could also extend a C or C++ program with traditional 1990s/2000s style 'plugins' written in almost anything that can get the required ABI out into a dll/so and load, unload, reload, etc. those at runtime without stopping the main program.
[0] - https://wiki.beyondunreal.com/UnrealScript
[1] - https://api.unrealengine.com/udk/Three/UnrealScriptReference...
[3] - https://twistedmatrix.com/users/glyph/rant/extendit.html
val s = "String"
val s:String = "String"But big, successful programs will often do (2).
Not having to write down the type isn't the same as the type not being determined at compile time, which is what "static" means.
--
[0] - http://mypy-lang.org/
I was more annoyed that it was practically unusable for years. Saner defaults, bug fixes and new types made it finally useful in late 2017.
I've never had it prevent a problem. I like staticly/strongly typed languages for this reason and putting optional type annotations into a language is never going to work out imo.
In particular, if Python added support for Go-like interfaces and recursive types, it wouldn't fall over for ~99% of nontrivial cases.
I think the type checking community also has quite a ways to go when it comes to asynchronous code. It becomes quite worthless to check that a future is being returned by a function, but it could be more helpful to know what that future will eventually yield.
Facebook also built Flow, a type checker for Javascript [1].
It's a language that let you start small, and progress a lot with the complexity of your code. You can be productive in Python in 3 days if you know another language. But you can still learn new Python useful things 10 years after you started.
The progress curve is very sane.
And in the same way, your project may start small, then you add docstrings, classes, modules, packaging, unittests, infrastructure... And at some point, you may want types.
I use types on maybe 10% of my code in Python. It's great it's not mandatory. And it's great it's here when I benefit from it.
Without types, if I have the code `a = foo(x=1)` then I have to hunt down the source file for `foo()`, which likely just returns `bar(x)`, so I have to hunt down the source file for `bar()` to figure out what the hell its return type is, and so on and so forth. With types, I just look at the type signature for `foo()` and I'm good to go (and again, editor integration means that I don't even need to look up `foo()` at all!).
YMMV.
It depends of the project. If you write a lot of flask/django code, writing the types is not that worth it except for a few functions/methods.
> Without types, if I have the code `a = foo(x=1)` then I have to hunt down the source file for `foo()`
No, you just hover the function and get the help() out of it in most framework and libs. Again, if your code is mainly using a well define, documented and popular framework/lib/api, that's not a big deal. And it certainly doesn't require YOU to add types.
Or if you write a program that is contained in 1 to 5 files top. Not use for types.
Or if you are writing your program in jupyter.
And you most likely copy a snipet from the doc anyway. After all, if you see that the function you want to use return a AbstractTranscientVectorServiceFactory object, you can't do much with the information without the doc anyway.
But let's be real, most functions in Python are named pretty explicitly, and return things that you expect like "iterable of numbers" or "file like object yielding utf8".
Types are particularly useful in the cases if you are in a big project with a lot of custom code or in a domain either very complex or that you don't master very well. They are a good for of safety net and documentation at the same time.
But they come at a cost and it's a good thing to be able to choose.
I program Python for 24 years now. It is my preferred language, but just recently I could go back to develop in it. It is impressive how much new idioms there are to learn.
we love types. They help us ship stuff faster.
I'm rooting for Reason, but it has a few nontrivial hills to climb before it's practical.
Well, it depends on the problem! If you’re working with a lot of data structures, or with bytes and serialization, compiled system languages with static typing are going to be productivity boosts over python. Languages aren’t everything, but there are definitely poor language/problem space fits.
You make an excellent point here that I don't see articulated very often. The Landscape of Popular Languages, let's say C/C++/Java/Python/Ruby/JavaScript, has a big gap in the middle. You have good choices between:
1. lower level "systems" oriented languages with static types, usually compiled, like C++. You get lots of flexibility and direct access to primitives. Static types help wrangle big codebases. Generally suited to large projects.
2. higher level "scripting" oriented languages with dynamic types, usually interpreted, like Python. Writing code for most tasks is easier. You give up some stuff you'd want for projects like operating systems or databases. Most projects aren't operating systems or databases, so that's usually a good tradeoff. Generally suited to small projects.
The problem is that lots of projects are medium-ish. You set out to build your web service backend or whatever, it would be a pain in the ass to write in C++, so you use Python. Getting it working is quick and easy. A few months later it's big, complex piece of software and working on it in Python is a pain in the ass. You can't win. What you really wanted was a language that's "easy to write" like Python, but with static or optional types, maybe better thread handling, and at this point the interpreter isn't doing much for you so it might as well be compiled. There are tons of cases where you just want a "better C" or "Python but faster and with static types", and for the longest time the Landscape of Popular Languages just had a giant hole there.
We needed that space filled and Go delivered. I'm usually very critical of Go, but I can't hate on it for being the wrong kind of language. It's definitely the right kind of language for these "goldilocks" problems that aren't too high or too low level, too big or too small. Part of being a good programmer is understanding that languages are tools, and you need to pick one that fits your problem. Go deserves all the success and praise it's gotten for being a language that fits actual problems.
The point of type-checking is that the function needs to work on a duck, then there is no point to ever pass it anything except a duck. In fact,the compiler should not even let you pass it something that's not a duck, because it's so pointless. That's literally the start and end of static typing, and if that's "rigorous" then yes, the whole point of static typing is to introduce this very basic level of rigor into your codebase. Because it's not going to work regardless of whether it passes the compiler.
Pretending interfaces do not exist does not actually make them go away. There is an interface there whether you explicitly enumerate it or not... even duck typing will fail if you try to call duck functions on something that is not a duck. Dynamic typing is not magic, it's the equivalent of passing everything around as Object or String in a static language. And that's an anti-pattern.
http://wiki.c2.com/?StringlyTyped
If you just want something to compile, you can pass in null-values of the appropriate type.
Now: there is a valid complaint that Java in particular really embraces the architecture-astronaut philosophy where everything is an overly-abstracted AbstractSingletonProxyFactoryBean (a convenient superclass for FactoryBean types that produce singleton-scoped proxy objects!). But usually it's fairly simple to wall that badness off from your actual business logic.
Moreover I think that at the time there were no statically typed languages that targeted web.
- ruby
- python
- Javascript
I was on a quest for a good, well supported, statically typed scripting language for quite a while, and in the end I defaulted to python.
On the other hand, I don't agree with some of the comments here. For example, Flow is not terminal only at all, I never use the terminal to run Flow. The editor integration is totally fine, especially in Atom and VSCode.
That being said, while I started out using Flow, TypeScript just has way more community adoption and better tooling. So at this point, I usually recommend TS over Flow to most people. But using either of them is way better than writing just regular JS code.
# Totoal #
Flow: 2081 open, 2748 closed
Typescript: 2541 open, 14421 closed
# Between 4/11 and 5/11 #
Flow: 88 closed, 93 new
Typescript: 448 closed, 173 new
Note: We are using flow but we are not happy that Flow is not up to speed with answering questions or addressing concerns.
That being said, Flow is better then no typechecks, and it was half a year ago that I looked, stuff might have improved.
The language server / editor integrations are an interesting goal and that seems to be why they have the watchman stuff in there.
I was initially kinda put off by that, as tools that watch for file events never end up working for me because I save like every 10 seconds.
Edit: for the active file / LSP part, I mean it shows errors mainly for the active file.
Edit: pyre will show type errors for all files in your repository, not just the ones you have open.
It actually makes ascii move around so that someone can pause the "video" and copy/paste out of it! Thats so cool!
Either you create a codebase strictly modularized respecting the lack of types and the 10000LOC speed limit or you change language. Golang is not fancy but it is really pragmatical and could appeal to the dynamic language crowd.
The other choices are Java/D/Scala. Or one can use Python as a glue language (superpowered C written modules used by Python). This is the problem/solution with Lisp too. If you go dynamic, you should be very careful, but there are gains. Don't forget to write tests unless you intend for a Matlab style experience.
I work in a decade-old Python codebase that is now up to 30m LOC. Our 2000+ developers are doing 15k commits a week, with continuous deployment.
(I gave a talk on this at PyData London two weeks ago)
Do you work this way?
The type checker obviously has to be run in continuous integration so it's not like the annotations are going to get outdated just because they are in comments. (Actually you shouldn't see them as comments, they are as much code as the rest of your code)
A new language will have few people who can support the code. An old language will have many.
def myfunc(foo: str, bar: int) -> Tuple[str]:
# ... > python --version
Python 3.6.1
> python -m pip install pyre-check
Collecting pyre-check
Could not find a version that satisfies the requirement pyre-check (from versions: )
No matching distribution found for pyre-checkhttps://pyre-check.org/docs/installation.html#building-from-...
Had been briefly discussed a few months ago on HN [0] but I guess I missed it. Always looking for some variety in static site/docs deployment!
At the start, those languages tended to be used for 100-line, 1000-line projects. They work really well in those domains. 5K lines works fine for single person projects too.
Once you get to 10K- and 100K- line projects, and you have 10+ people on a project, types start to make sense. You can't change 10K lines of code at once, so you might as well have some rigidity.
Also note that you can do a lot more in 10K lines of Python than 10K lines of Java, C or C++ -- and in the 90's, when those languages came up, those were basically your choices.
I honestly can’t think of anybody in my career who’s been comfortable with dynamic languages that had a desire to move to static. It’s such an impediment to the entire programming style that it doesn’t naturally happen.
On the flip side, I know plenty of static typing people who don’t seem to think they can function without it.
No matter what your preferred language, Python and JavaScript are almost unavoidable and because of that I think you see a lot of stuff like this brought to the table to help make people more comfortable.
Python for sysadmin, math, ML, etc. Javascript for browser.
You see a lot of the same thing in the Elixir community with its gradual type system. I can’t tell you how many times I’ve seen the discussion from people who want it to be statically typed, but neglect that all of the guarantees from it go out the window with distributed nodes.
Really? Anecdotally, I have the exact opposite experience: I know many devs (myself included) who had always used dynamically typed languages but got "hooked" on static typing after trying it in a decent language (Swift in my case), but I can't name a single person who went the other way.
In my experience, if you use a modern statically typed language with a solid type system, after the initial learning curve, the type system stops being an impediment to probably 95% of the code you write. In return, you get some really nice guarantees about your code, and what would be large and tedious refactors in a dynamically typed language now become a breeze. And if you bolt static typing onto a dynamically typed language, you get the best of both worlds: safety guarantees by default, and the full expressiveness of the underlying language when you need it.
Personally, I'm excited for these tools because I write code in dynamically typed languages every day, but I strongly value the benefits of static typing. This way, I can have my cake and eat it, too.
Every statically typed language I've worked with on the web just ends up forcing you to duplicate the same already defined structure in multiple places, writing a ton of extra code that provides marginal benefit but creates a major negative impact on productivity.
For many other areas, especially on phones, embedded devices or desktop software static types will make a lot more sense.
I think languages where the primary focus is data exchange the benefits are less pronounced. That's just my experience though.
In my projects I have dozen of classes that are nearly strings but add functionality not present in strings. Trying to type check those would turn into insanity pretty quickly.
I'm someone who would be described as a pythonist. I learned CS in python, had a quick foray into Java (which I'm not particularly fond of), and then have done the vast majority of my coding, both personal and professional, in python. I'm a huge proponent of type hinting.
Reasons for this:
- It's not really an impediment. Quality code should already have APIs notated with argument and return types. Converting docstrings to mypy is easy.
- It's optional. You have some weird super dynamic magic nonsense. Cool, annotations are optional. Don't include them on your metaclass-generating decorator function. Being able to opt out of the safety guarantees easily is really really useful for those cases where you do want to abuse dynamism.
- Its super useful. I catch bugs faster now. I write less buggy code. Refactoring is much, much easier (mypy highlights the lines where I'm now doing bad attribute accesses etc.). Some of these things can be provided by a good ide, but I'm often not in an IDE, and this way I can run it as a pre-commit hook.
Agreed that for sysadmin work its maybe not as helpful. For math and ML, I think it is. There are issues that make numpy/tensorflow really difficult to typecheck internally, but there's active work on that front as far as I know.
I don't know whether this is an unpopular opinion (seems like it might be?) but I would never tell anyone to start with a dynamically typed language.
But it's not binary and there are plenty of good reasons to have static type checking. I personally went through an exercise where I applied type annotations to a large Python project and found a good amount of bugs just by type checking.
I think having the flexibility to add type annotations later, only apply to parts of a code base, and allow some violations is a great middle ground and makes Python a much more attractive option for large code bases.
I am however pretty unconvinced by the superiority of static typing. Being able to let the compiler verify the types for me in compartmentalised pieces of my software is very nice an all that, but for me I doubt it has caught many bugs.
I think a lot before writing code, and what comes out usually works on the first or second try.
1) Performance. We needed something that would consistently work quickly on Instagram's server codebase (currently at several million lines).
2) We are building deeper semantic static analysis tools on top of Pyre. We've built some of these tools for Hack/PHP already, so following the Hack type checker's architecture is the best way for us to achieve this.
That's not really an answer to why you didn't work on mypy, at least to an outsider to the decision making process. Are you saying that you discovered it's just not possible to scale mypy (or at least not without extensive work / more work than building your own solution?)
I can appreciate the choice in context of 2) :)
Full disclosure: I worked on the Hack type checker briefly, a long time ago :)
> Internally, Pyre's high-level architecture is similar to that of Hack, Facebook's type checker for PHP.
If they had a performant codebase to start with, this makes a lot of sense.
Apple: LLVM (I know I’m stretching the definition here :) ); Objective-C, Swift; N/A; Cocoa.
Microsoft: .NET CLR; Visual Basic, C#, F#; ASP.NET; N/A.
Facebook: HHVM; Hack; N/A; React.
Google: Go, Dart; Golang, Dartlang; GWT, Guava; Angular; Android, Flutter.
Oracle: JVM; Java; APEX; N/A.
It seems that for some reason just Amazon doesn’t want to play :)
Microsoft: WPF, Blazor Oracle: JavaFX
Edit: oh and copyright
Still, annotation/inference experience falls apart completely when interfacing with libraries like SQL Alchemy or boto3. Supposedly writing custom plugins is the way, but that never gets done! How will pyre handle stuff like this, or is it just asking too much? Perhaps a combination of better tooling and better library authoring, eschewing the temptation of meta programming and dynanimo, to play well with type hints will be necessary?
I'm excited for these new tools and will give it a play. However I honestly hope I never have to work in a python-forward environment again.
Also, MonkeyType will allow you to add types to your Python based on types inferred at runtime: https://github.com/Instagram/MonkeyType
The system first starts by allocating a large area in shared memory (through a call to mmap). That area is very large but because most of it wont be written to it’s ok in practice.
After that, the program forks as many times as there are cores. Each of those cores are called “workers”. The first program is now the master.
The master and the workers communicate through pipes, but that is only used for synchronization. The lion share of the data goes through that shared memory that was mmaped at the beginning.
There are 2 main things shared in that area. 1- atomic hashtables of serialized ocaml objects (you can define as many as you like with a functor) 2- an atomic table of dependencies.
Each workers can read and write to those tables without locks (but only the master can remove from them).
It turns out that that setup works well in practice. Serializing/deserializing costs are mitigated by a cache of deserialized values for each core. And this way each core can manage there memory (the gc does not need to scan the shared memory).
Because that setup was working well in practice, it was reused by Flow and now Pyre. We refer to that setup internally as the “Hack infrastructure”.
I hope adding types to your library becomes the norm in Python as well, because as it stands, very few Python libraries have types defined. This means you can only have type guarantees in the code you write and not in that of your dependencies.
I will never use Oracle products or allow them to bleed into my infrastructure for any reason for example.
It's possible that this has saved my company a lot of money, it's also possible that it was completely unjustified, but given the trend of the company in question- I believe it was a positive decision. Make choices, the best you can in the moment, you can usually revisit them later.
There are many companies which should not get an ounce of that kind of trust, regardless of how useful their products are right now; very many simply can’t be trusted, for a myriad of different reasons.
[1] https://docs.python.org/3/library/typing.html#module-typing
(I might have somehow missed the full docs - in that case, if anyone has a link, I'd be grateful.)
edit: Also, was I correct in that it's basically "The stuff that's specified in the PEP and works in mypy should work"?
Aside from that, pyre looks like a super useful tool. Hopefully it has fewer rough edges than mypy.
I know it's probably better than nothing but if the same problems carry through, it'll be a pain.
These are all tractable problems, so I don’t see a theoretical problem; however without more info on your flow issues I can’t make a good comparison.
Edit: I did skim through the comments here and also skimmed through the official site and the GitHub repo. I didn't find anything about this name.
The person who came up with this name didn't think it through.
I've tried it back when we were using PySpark and it did what I expected, but I am not the heaviest consumer of Jupyter notebooks to be able to say if it's 80/20 or 100% of what one would expect
$ pip install pyre-check
Collecting pyre-check
Could not find a version that satisfies the requirement pyre-check (from versions: )
No matching distribution found for pyre-check
(Installed fine on an my work machine running OSX 10.13.3.)
I tried to build from source but got another error after some time:
File "ast/astStatement.ml", line 289, characters 41-74:
Error: Unbound module Recognized
With that said, the real answer is 'it depends', and it may well be the case that mypy serves your needs better.
Update: for the downvoters, the PEP listed the python version for 3.5 here https://www.python.org/dev/peps/pep-0484/. Yes it does have a python 2.7 section but after Python 2.7 is discontinued pretty sure Python core team won't support type hints on 2.x. On top of that, not to mention the fact the type hint suggested on 2.x (as a comment) is different from the official 3.x syntax.
> Some tools may want to support type annotations in code that must be compatible with Python 2.7. For this purpose this PEP has a suggested (but not mandatory) extension where function annotations are placed in a # type: comment.
mypy supports those annotations for Python 2 code. Quoting http://mypy.readthedocs.io/en/latest/faq.html#how-do-i-type-... :
> How do I type check my Python 2 code?
> You can use a comment-based function annotation syntax and use the --py2 command-line option to type check your Python 2 code. You’ll also need to install typing for Python 2 via pip install typing.
https://github.com/google/pytype
It just doesn't seem to have gotten as much traction yet.
Supporting an entire new AST and type system (pattern matching) is a large investment. It can be made if there's enough of a userbase out there to justify it. That doesn't seem to be the case. Not yet at least.
It is also open source.
example?
we are working on an extension that will add the inferred types as annotations to your code.
It's not about the concrete types but instead about what protocols it supports.
Let me repeat: Python has no types.
It has built in classes that used to be types 15 years ago, but no types. [0]
90% of the holy war between strongly and weakly typed in python would be resolved if we just removed all references for types from Python, and renamed TypeError to UnsupportedOperand.
Pep 484 [1] is about class hints, and this software builds on top of that. That has it's place, but it's an ugly hack that should not become a main feature of the language.
[0] https://www.python.org/download/releases/2.2/descrintro/#int...
[1] https://www.python.org/dev/peps/pep-0484/#type-definition-sy...