Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Erg: a statically typed language that is Python compatible

github.com

Post reply on HN
Print view View original

171–180 of 194 posts

Re: Erg: a statically typed language that is Python compatible

#171

Post by treesprite82 »

smt88 wrote: post #157
ptx wrote: post #125

Earlier quoted context omitted.

And yet I notice that you separated the paragraphs in your post using semantic whitespace rather than "BEGIN PARAGRAPH" / "END PARAGRAPH" or something similar, and it seems perfectly readable to me.

> separated the paragraphs in your post using semantic whitespace That's not what "semantic" means. In my post, the size of the whitespace was not semantic. I could have used one spaces, two spaces, tabs, or (as I did) a couple of newlines. All that matters is that there was any whitespace at all -- which is what most mainstream languages do. In Python, the whitespace I chose would change the actual program. To repea…

> a couple of newlines

A couple of newlines to create a new paragraph is semantic whitespace, as one newline or a space would not do so. Markdown (although not HN's Markdownesque syntax) even has significant trailing whitespace, which I would object to in a programming language.

> it's much harder to tell the difference between " " and " ".

Can't think of any scenario where you'd need to.

If you do mix hard tabs with spaces for indentation, which would cause readability issues with other languages anyway, it'll fail to run and point out where.

I can empathize that significant whitespace sounds off-putting at first, but after biting the bullet I think it's definitely a net positive. Indentation indicates my intent yet most languages just ignore it. For example, consider this gotcha across multiple non-significant-whitespace C-like languages:

    for (i = 1; i
Or, alternatively, hunting down one misplaced closing bracket.

Also, with Python appealing to new programmers, there'd probably otherwise be plenty of beginner code with no indentation at all.

Re: Erg: a statically typed language that is Python compatible

#172

Post by bb88 »

elcritch wrote: post #136
bb88 wrote: post #106

Earlier quoted context omitted.

> I really want to try making a native KiCad autorouter. But I don't want to figure out the C++ plugin setup and since KiCad 6 the Python APIs seem better documented and supported anyways. So I find this to be super interesting, particularly when it comes to parts with lots of pads that one has to route. Python would let you iterate the algorithm quickly. It's far easier to optimize the big O notation of your autorou…

Thanks! Good to hear others would be interested in something like that. It's one of those borderline "oh man that would be nice". > Python would let you iterate the algorithm quickly. It's far easier to optimize the big O notation of your autorouter than in C++, say. The hard part wouldn't be the routing algorithm itself. It's getting the algorithm and code to handle all of the corner cases. That's really what has ke…

In that case I would wrap it with a class to enjoy programming with the reference counted python garbage collector here.

    from cython.cimports.cpython.mem import PyMem_Malloc, PyMem_Free

    @cython.cclass
    class SomeMemory:
        data: cython.p_double
    
        def __cinit__(self, number: cython.size_t):
            # allocate some memory (uninitialised, may contain arbitrary data)
            self.data = cython.cast(cython.p_double, PyMem_Malloc(
                number * cython.sizeof(cython.double)))
            if not self.data:
                raise MemoryError()

    
        def __dealloc__(self):
            PyMem_Free(self.data)  # no-op if self.data is NULL
Extending it into a typical python array type doesn't look that hard. Just need to map the appropriate dunder functions into C array operations. Then optimized functions can directly interact with the C types. Basically any utility function you might need with C data types you would just add to the class.

And at that point, you're back to coding in regular python again.

I hope this helps but good luck with your project no matter which option you take.

Re: Erg: a statically typed language that is Python compatible

#173

Post by joshuamorton »

mdaniel wrote: post #101
joshuamorton wrote: post #47

Earlier quoted context omitted.

> Oh, and don't forget to check all the possible code paths that lead to this to make sure you've exhausted all possibilities." This is literally what mypy does. There's no difference between a mypy-enabled codebase and a java codebase in terms of static typing (other than that mypy actually supports a generally richer type system). Like yes if you aren't validating the type hints you aren't getting the value, but if…

> There's no difference between a mypy-enabled codebase and a java codebase in terms of static typing (other than that mypy actually supports a generally richer type system). that must require some advanced usage of mypy then, because my experience was that even the most simple example got the finger from mypy that would have very obviously worked in Java mkdir alpha echo 'beta = True' > alpha/models.py echo 'from .m…

I mean I think python's module's are kind of stupid, but even as someone who literally doesn't every use python's module system, my very first thought here was "I bet strict mode is requiring explicit exports in __all__"

And indeed[0] that's the case. It makes perfect sense that the abstract machine of typed python does not allow everything that the abstract machine of untyped python does, and java would error on trying to use a private class or method just the same.

[0]: https://mypy.readthedocs.io/en/latest/command_line.html#cmdo...

Re: Erg: a statically typed language that is Python compatible

#174

Post by joshuamorton »

smabie wrote: post #119
joshuamorton wrote: post #47

Earlier quoted context omitted.

> Oh, and don't forget to check all the possible code paths that lead to this to make sure you've exhausted all possibilities." This is literally what mypy does. There's no difference between a mypy-enabled codebase and a java codebase in terms of static typing (other than that mypy actually supports a generally richer type system). Like yes if you aren't validating the type hints you aren't getting the value, but if…

The number of "# type: ignore" comments I've seen in all python codebases that use mypy seems to disagree. mypy is laughably primitive compared to advanced static typing systems: Rust, Haskell, OCaml, etc

> mypy is laughably primitive compared to advanced static typing systems

I don't disagree, but that's not an argument I ever put forth! (and I actually sort of disagree a little bit, mypy has/is getting a bunch of really cool powerful features that put it in the realm of "as cool as" those languages: PEPs 544, 586, 591, 647 (this is a weak form of contract types!), 675 (~constexpr string type), 646 (variadic generic/numeric dependent types!))

Re: Erg: a statically typed language that is Python compatible

#175

Post by FridgeSeal »

joshuamorton wrote: post #168
FridgeSeal wrote: post #90

Earlier quoted context omitted.

Sorry, but MyPy and friends can barely hold a candle to what actual static-typing systems do - Rust, Haskell, OCaml, Typescript, even .Net (C#/F#) offer more safety and guarantees. Type hints in python are _just that_, they're hints. The whole "typed" python ecosystem relies on packages and the language using them, using them correctly, and using them consistently. In my experience so far, I've seen little widespread…

> Sorry, but MyPy and friends can barely hold a candle to what actual static-typing systems do - Rust, Haskell, OCaml, Typescript, even .Net (C#/F#) offer more safety and guarantees. Note that you don't include the most common static languages there (cpp, java, golang), you include languages known *specifically " for their extremely powerful type systems, one of which , just like mypy, uses gradual typing! This suppo…

I mean sure, we can include C++, go and java in there if you want? I don’t really know what the point you’re making here is?

> one of which , just like mypy, uses gradual typing!

This is like arguing that because your scooter also has a petrol engine, it’s as fast and efficient as an F1 car. My argument was that MyPy doesn’t compete with the capabilities of modern statically typed languages. TS might also technically be gradually typed, but most devs I know just go straight to fully typed TS, because working in a mix/gradual environment is painful and the community uptake of strict types is far higher.

Re: Erg: a statically typed language that is Python compatible

#176

Post by joshuamorton »

FridgeSeal wrote: post #175
joshuamorton wrote: post #168

Earlier quoted context omitted.

> Sorry, but MyPy and friends can barely hold a candle to what actual static-typing systems do - Rust, Haskell, OCaml, Typescript, even .Net (C#/F#) offer more safety and guarantees. Note that you don't include the most common static languages there (cpp, java, golang), you include languages known *specifically " for their extremely powerful type systems, one of which , just like mypy, uses gradual typing! This suppo…

I mean sure, we can include C++, go and java in there if you want? I don’t really know what the point you’re making here is? > one of which , just like mypy, uses gradual typing! This is like arguing that because your scooter also has a petrol engine, it’s as fast and efficient as an F1 car. My argument was that MyPy doesn’t compete with the capabilities of modern statically typed languages. TS might also technically…

What features that Javas type system provides does pythons lack?

I can name dozens that python has that Java doesn't. My point is that if you include cpp or java or golang the statement becomes false. Python's type system is actually generally speaking more robust than those (cpp is comparable, but I don't think python's is worse).

So I'm asking, be specific what capabilities does mypy lack that cpp or java or golang provide? Keep in mind, mypy supports literal types, limited dependent types, dynamic-duck typing (protocols), limited contract types, and more. Java doesn't, go doesn't. Cpp supports some of those but it requires arcane incantations.

Re: Erg: a statically typed language that is Python compatible

#177

Post by still_grokking »

mdaniel wrote: post #158
still_grokking wrote: post #110

Earlier quoted context omitted.

It's imho especially ridiculous to say some linter, that needs "hints" and annotations everywhere, is comparable to a static type system when looking at modern static languages, which have usually very strong type inference . The point of a sound static type system is that you get a guaranty that your program is type-safe even in case not everything is "hinted properly". With the linter approach on the other hands si…

Did you reply to the right person? I'm with you, friend :-)

I think I did not object anything you've said. :-)

I only wanted to point out once more that a proper static type system is of more use than some bolted on linter. (And add the point about type inference).

Re: Erg: a statically typed language that is Python compatible

#179

Post by still_grokking »

joshuamorton wrote: post #169
still_grokking wrote: post #110

Earlier quoted context omitted.

It's imho especially ridiculous to say some linter, that needs "hints" and annotations everywhere, is comparable to a static type system when looking at modern static languages, which have usually very strong type inference . The point of a sound static type system is that you get a guaranty that your program is type-safe even in case not everything is "hinted properly". With the linter approach on the other hands si…

What is the difference between a "linter" and a "static type system"? Be specific? Pytype, an alternative python "linter" provides type inference. So it's not that. The best I can come up with is toolchain integration, which is exactly what I said .

TL;DR: I would say the difference is the level of confidence in the results of type-checking you'll get.

Of course an external tool could model and check against a proper type system, in theory. So that's indeed not the point.

A proper static type system comes with a formal definition and (math-like) proves of soundness (and progress). This will give you the guaranty that a well typed program is sound.

A "linter" can't give you that guaranty. All it can do is to say "LGTM"; but your program could still crash or bug-out in some other way at runtime. That's quite a big difference imho.

Linters are more like automated tests: They may tell you something is wrong, but they don't give any guaranties that things are actually right. A proper static type system OTOH gives such guaranties.

For example I would consider TypeScript being only a very funky linter—as it does not model a sound type system. My understanding is that mypy and friends are not different. All those linters produce not only way to much false positives, no, they also produce false negatives (meaning that they let unsound programs pass; something that can not happen with a formally verified type system).

As an anecdote, I got bitten by that when trying TS (and it was a very sad experience): When playing around with TS for the first time I did not know that TypeScript is barely a linter. I was really very excited about all those things you can do with proper structural types there! I was coming from Scala 2 which has only very limited support (based on JVM reflection) for this kind of types¹. But I always loved the "objects as hash-maps" concept of JS… So I've written some small REST client for one of our back-end services in TS. Everything nicely typed, no escape hatches used. Someone also told me I have to use "stric mode" which will "catch all type errors". That looked a bit odd, but OK JS was not made to be typed in the first place. Everything looked great than. As someone coming form the purely functional Scala camp (where things work when they compile :-D), and encouraged by all those people praising TS for its "powerful type system", I've put the same amount of confidence as in Scala into the typed code I've written in TS. By this I mean you don't need to double check whether things are correct if the typer says they're correct. It's enough to check the logic of your program. You don't have to try out "manually" (this includes written tests!) every line of code. Up to than everything looked good. So I've pushed things and started to do end-to-end test. That was when I fell out of my dress. My code produced runtime errors which where actually "impossible"! The TS "type-checker" said things are such and such but at runtime they were different (which I found out only after some deep debugging sessions as this was something I did not expect in any way)! I think I've wasted one and a half day debugging this shit only to find out that TS "types" are actually worthless. If I have to try out any and every line of code manual anyway what's the point of TS? I could have written this thing in pure JS (where I have to also check any and every line manually), but it would have been much easier without "wrestling" with that quite useless "type system"… :-(

The point is: A dynamic language remains a dynamic language even if you use some linter! Without true guaranties you can't have much additional confidence in your code without testing just everything—even the parts that were already "tested" by our "type system". Actually it's even worse than without a linter if you don't know about its shortcomings and make the mistake to blindly trust such a tool; like you can do in case of a sound type system (modulo the very seldom cases of compiler bugs).

I hope I could make it now more understandable what I mean by "proper static type system".

___

¹ Things improved in Scala 3 though.

Re: Erg: a statically typed language that is Python compatible

#180

Post by joshuamorton »

still_grokking wrote: post #179
joshuamorton wrote: post #169

Earlier quoted context omitted.

What is the difference between a "linter" and a "static type system"? Be specific? Pytype, an alternative python "linter" provides type inference. So it's not that. The best I can come up with is toolchain integration, which is exactly what I said .

TL;DR: I would say the difference is the level of confidence in the results of type-checking you'll get. Of course an external tool could model and check against a proper type system, in theory. So that's indeed not the point. A proper static type system comes with a formal definition and (math-like) proves of soundness (and progress). This will give you the guaranty that a well typed program is sound. A "linter" can…

> My understanding is that mypy and friends are not different. All those linters produce not only way to much false positives, no, they also produce false negatives (meaning that they let unsound programs pass; something that can not happen with a formally verified type system).

I'm pretty sure the mypy and typescript devs would disagree here. The typescript and mypy abstract machines aren't any less sound than Java or c++.

All four are abstract machines that make fundamentally similar guarantees. Cpp and Java can still encounter classcast exceptions and segfaults.

And, like, you still need tests in functional languages. Specifically, I don't think I've encountered anything like

> My code produced runtime errors which where actually "impossible"! The TS "type-checker" said things are such and such but at runtime they were different

Without either explicitly subverting the type system, or dealing with some kind of untyped deserialization along an api boundary, which you absolutely need to test in any language.

Post reply on HN