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

Revenge of the Types

lucumr.pocoo.org

Post reply on HN
Print view View original

21–30 of 137 posts

Re: Revenge of the Types

#21

Post by seanmcdirmid »

bjourne wrote: post #11

Armin didn't address what I belive is the main point of adding type annotations to Python: compiler checkable documentation and as hints to IDE:s. Seen in that perspective, a sucky type system is good enough because it's use isn't to verify program correctness. Personally, I think a standardized format for describing types in docstrings would be 100x better but that's not the way the Python core devs have choosen. An…

Yes. If you believe the point of a type system is to enforce correctness, then this doesn't make sense. Most type theorists seem to take this position. But if you believe that the point of a type system is to provide programmers with better feedback, then this completely makes sense. I wish more type systems research would explore on the latter rather than fixating on the former.

Typescript and Dart have been developed with similar philosophies.

Re: Revenge of the Types

#22

Post by thiagof »

pjungwir wrote: post #7

Random question for the type experts out there: is there any language that lets me track the units of my numeric variables? For instance, something like this: float drop(float x0, float duration) { float x = x0; float t = 0; float v = 0; float g = -10; float dt = 0.01; while (t /1000 ); // abbrev for a cast: (float ).001 } Then I want the compiler to check that I'm not mixing up my units. It seems like this would be…

Something like this in Rust: https://blog.mozilla.org/research/2014/06/23/static-checking...

Re: Revenge of the Types

#23

Post by ivoras »

Not only that, but look at the niche Python is occupying. It's a well established and respected niche to which, by definition, the language is suited very well.

By adding static types, the focus of the language would move to a different niche, which would probably be already occupied by some competitor language(s) which do(es) types much better.

If you want sort-of Python-ish syntax with elaborate types, just use Nimrod and leave Python alone. Get the right tool for the job, don't mutilate a perfectly good existing tool.

Re: Revenge of the Types

#24

Post by tosh »

If you want to learn more about how 'optional' and 'unsound' type systems can still deliver a lot of value there are some interesting articles on Dart's optional types:

* http://journal.stuffwithstuff.com/2011/10/21/wrapping-my-hea...

* https://www.dartlang.org/articles/why-dart-types/

* https://www.dartlang.org/articles/optional-types/

Re: Revenge of the Types

#25

Post by tikhonj »

pjungwir wrote: post #7

Random question for the type experts out there: is there any language that lets me track the units of my numeric variables? For instance, something like this: float drop(float x0, float duration) { float x = x0; float t = 0; float v = 0; float g = -10; float dt = 0.01; while (t /1000 ); // abbrev for a cast: (float ).001 } Then I want the compiler to check that I'm not mixing up my units. It seems like this would be…

Haskell has a few libraries to do this. I particularly like unittyped[1], which not only keeps track of units but also converts among compatible ones automatically. So 1 meter + 1 inch would typecheck and be converted automatically, but 1 meter + 1 second would give you a type error.

The wiki page[2] has a bunch of examples, which I find pretty compelling. The one problem is that error messages are ugly, but they're ugly in a consistent way. You can just ignore the ugliness as unnecessary noise.

    *Main> (1 meter / second) * 5 second
    5.0 m/s⋅s
    *Main> 2 meter + (1 meter / second) * 5 second
     7.0 m
One cute thing is that prefixes like "kilo" are just functions, letting you write things like:

    *Main> (42 kilo meter) `as` mile
    26.097590073968025 mile
    *Main> gallon `as` (cubic (deci meter))
    4.546089999999999 dm⋅dm⋅dm⋅#
Haskell is really good at dealing with numeric types in general. For example, it's quite easy for a library to define its own types, which then behave just like built-in ones including nice syntax. Unittyped follows this philosophy, letting you use units with things that aren't floats, like rational numbers, meaning you don't have to lose precision.

    *Main>  (1 % 2) . meter `as` foot
    625 % 381 ft
It's a really slick design and manages to give you safety as well as additional expressivity (since units get converted automatically).

[1]: https://hackage.haskell.org/package/unittyped

Re: Revenge of the Types

#26

Post by Dn_Ab »

thelinked wrote: post #10
pjungwir wrote: post #7

Random question for the type experts out there: is there any language that lets me track the units of my numeric variables? For instance, something like this: float drop(float x0, float duration) { float x = x0; float t = 0; float v = 0; float g = -10; float dt = 0.01; while (t /1000 ); // abbrev for a cast: (float ).001 } Then I want the compiler to check that I'm not mixing up my units. It seems like this would be…

Check out F#'s units of measure. http://msdn.microsoft.com/en-us/library/dd233243.aspx

pjungwir's example code is actually really close to what you'd see in F#. In F# you'd typically write it in a more functional way with say a recursive inner function but I'll leave it imperative for clarity's sake:

    [] type s
    [] type m
    [] type km  

    let mtokm (x:float) = x * 1./1000.
   
    //the types of g and ground are inferred
    let drop g ground (x0:float) =
         let mutable x = x0  //type inferred here
         let mutable t = 0.0
         let mutable v = 0.0 
         let dt = 0.01

         while x >= ground  do
            v  drop -10.0 0. 50.  
   val it : float = 3.16

Re: Revenge of the Types

#27

Post by eliben »

mmagin wrote: post #6

I didn't know Python users hate static typing so much.

"Python users" is a vast generalization (this is literally one of the most popular programming languages in the world - there are a lot of users), and "hate" is a strong word. So if you want to convey meaning in your comment, you should try to be less hyperbolic.

FWIW: I'd argue that most "users" of Python don't know the difference between static and dynamic typing. Or care about fanatic language wars in which the word "hate" is used to describe preferences between purely technical details.

Re: Revenge of the Types

#28

Post by com2kid »

pjungwir wrote: post #7

Random question for the type experts out there: is there any language that lets me track the units of my numeric variables? For instance, something like this: float drop(float x0, float duration) { float x = x0; float t = 0; float v = 0; float g = -10; float dt = 0.01; while (t /1000 ); // abbrev for a cast: (float ).001 } Then I want the compiler to check that I'm not mixing up my units. It seems like this would be…

Ada also allows this. Has for quite some time, and it comes with a built in real world units system.

Re: Revenge of the Types

#29

Post by antrix »

pjungwir wrote: post #7

Random question for the type experts out there: is there any language that lets me track the units of my numeric variables? For instance, something like this: float drop(float x0, float duration) { float x = x0; float t = 0; float v = 0; float g = -10; float dt = 0.01; while (t /1000 ); // abbrev for a cast: (float ).001 } Then I want the compiler to check that I'm not mixing up my units. It seems like this would be…

Java's pluggable type system can do this. The Checker framework provides a Units checker that can be plugged into the compile stage. See this blog for more info: http://blog.paralleluniverse.co/2014/05/01/modern-java/
Post reply on HN