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

Types

gist.github.com

Post reply on HN
Print view View original

71–80 of 198 posts

Re: Types

#71

Post by MrBuddyCasino »

lucian1900 wrote: post #70
ozy wrote: post #69

So what might make dynamic languages easier to write in? I enjoy dynamic languages more because: * "double kilometerToMiles(double km) { return km / 1.6 }" here the types are of really low value, yet I have to type them in. * a mutable list of generic and variable arity event handlers. Really hard to specify as a type (most languages cannot do it). Really easy to use. * co- and contravariance and lists, the math work…

Writing down the types isn't a necessary property of static type systems. In Haskell, F# or (OCa)ML, you almost never have to actually mention any types. I do agree that Java-style types aren't of much value. That catches few errors at significant cost.

Catching logical errors is only one out of several things that static typing gives you.

Incidentally, right now this is a few positions above this posting: https://news.ycombinator.com/item?id=12350063

Better IDE support, a kind of self-documentation and increased performance come to mind. I know there are counter-examples for each of these points, but the general trend cannot be denied.

Re: Types

#72

Post by icen »

twblalock wrote: post #13
_ibu9 wrote: post #6

Earlier quoted context omitted.

The missing explanation is that `smaller` is a third argument to the function. It's type is a proof that x In the case where the values are read from the external environment, first you would have to compare them before calling the function. The comparator would return either a proof that x y. In the first case you plug that value into the `smaller` argument, in the second case it's your responsibility to signal what…

What would happen if you did not compare them before calling the function, and just passed them in such that x >= y?

Nothing; it would return a partially applied function that waits for a proof that `x The key here is that `add` is not a function `Nat -> Nat -> Nat`, it is a function `(a : Nat) -> (b : Nat) -> LT a b -> Nat`. There are just some compiler features that allow you to avoid having to write out the full `LT a b` proof each time you want to add things!

Re: Types

#73

Post by one-more-minute »

If this topic interests you, Julia's type system is worth checking out [1]. Julia is unusual among dynamic languages not just for having a powerful type system (including parametric types), but also for making it idiomatic to make full use of types. Aside from the benefits to the programmer, this also allows the compiler to get to Rust-level performance where it's needed.

I find that this is a nice compromise that gets a lot of the benefits of static type systems (small, local errors as opposed to behavioural bugs, ability to express concepts and constraints) without the drawbacks (loss of interactivity, or inability to escape the type system when it's appropriate).

[1]: http://docs.julialang.org/en/latest/manual/types/

Re: Types

#74

Post by igravious »

jroesch wrote: post #39
seanwilson wrote: post #32

Earlier quoted context omitted.

Any examples? I'm curious for examples of a nontrivial type that would catch lots of common programming errors where the proofs can be automated. I see lots of new dependently typed languages but not much interest in addressing the proof automation aspect.

You don't need type theory to verify program properties, people have been using first-order methods for decades to prove properties about programs. For example there was a line of work in ACL2 that verified a microprocessor implementation, as well as plenty of modern work using tools like SMT to automatically prove program properties, see Dafny, F* for language based approaches. Though there is plenty of language agn…

If (like me) you didn't know what the abbreviation SMT stands for -- I looked it up and it is Shiver Me Timbers http://encyclopedia.thefreedictionary.com/Shiver+Me+Timbers Seems to be some kind of pirate speak.

Only kidding! It stands for Satisfiability Modulo Theories https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

“In computer science and mathematical logic, the satisfiability modulo theories (SMT) problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality. Examples of theories typically used in computer science are the theory of real numbers, the theory of integers, and the theories of various data structures such as lists, arrays, bit vectors and so on. SMT can be thought of as a form of the constraint satisfaction problem and thus a certain formalized approach to constraint programming.”

I'm not sure I'm any the wiser after that …

A notable building block appears to be SMT-LIB http://smtlib.cs.uiowa.edu/index.shtml

Re: Types

#75

Post by lmm »

one-more-minute wrote: post #73

If this topic interests you, Julia's type system is worth checking out [1]. Julia is unusual among dynamic languages not just for having a powerful type system (including parametric types), but also for making it idiomatic to make full use of types. Aside from the benefits to the programmer, this also allows the compiler to get to Rust-level performance where it's needed. I find that this is a nice compromise that ge…

It sounds very ad-hoc? (And Julia's benchmarking has not been reputable in the past, FWIW).

> without the drawbacks (loss of interactivity, or inability to escape the type system when it's appropriate).

One can absolutely have interactivity in a statically typed language, and virtually all statically typed languages support casting when you absolutely need to.

Re: Types

#76

Post by lmm »

twblalock wrote: post #28
seanwilson wrote: post #17

Earlier quoted context omitted.

> What would happen if you did not compare them before calling the function, and just passed them in such that x >= y? It would be a type error. All the compiler would know is that "x" and "y" are strings/integers so it would tell you they were the wrong type. If you do a branch on checking they are the correct type, then in that part of the branch the compiler will know they are the correct type and allow "add" to b…

Assuming they were integers before, what type would they become after they were compared?

An existential type - "some unknown types x (a subtype of integer) and y (a subtype of integer) for which LT x y" (or else the other branch). Languages designed for these techniques generally make it easier to write those types than it is in say Java (and in some languages it would be impossible to write that type at all) and infer them so you're not constantly writing them, though there's usually a way to express them directly/explicitly if you need to.

Re: Types

#77

Post by lmm »

titanomachy wrote: post #23

Someone who has experience with both Agda and Idris, could you comment on which is easier to get started with? Coming from a Haskell background, I'd like to try my hand at writing more interesting constraints into my types. Any experiences using these languages for (non-research) work? I've played around with Coq a little and it certainly feels more like a proof assistant than a programming language. It was fairly co…

I have very limited experience, but it's worth saying that Idris was designed by an experienced Haskell user with the intention of using it to write practical programs.

Re: Types

#78

Post by one-more-minute »

lmm wrote: post #75
one-more-minute wrote: post #73

If this topic interests you, Julia's type system is worth checking out [1]. Julia is unusual among dynamic languages not just for having a powerful type system (including parametric types), but also for making it idiomatic to make full use of types. Aside from the benefits to the programmer, this also allows the compiler to get to Rust-level performance where it's needed. I find that this is a nice compromise that ge…

It sounds very ad-hoc? (And Julia's benchmarking has not been reputable in the past, FWIW). > without the drawbacks (loss of interactivity, or inability to escape the type system when it's appropriate). One can absolutely have interactivity in a statically typed language, and virtually all statically typed languages support casting when you absolutely need to.

"Ad-hoc" seems subjective but to me it feels very carefully thought out. And while I've found the benchmarks to be accurate, I more importantly mean myself (and many others I know) being easily able to get high performance code when we need it.

My second paragraph was only a personal take on what works for me, so YMMV, but nevertheless: I'm not arguing against static type systems in principle, but these are practical concerns rather than theoretical ones. I don't know of a mainstream static language that supports a fully dynamic REPL (Haskell's isn't great) and casting back and forth to `interface{}`, `Object`, or `Any` everywhere is a huge overhead compared to duck typing. I look forward to a future language solving those issues, but that's not the case today.

Re: Types

#79

Post by lmm »

ozy wrote: post #69

So what might make dynamic languages easier to write in? I enjoy dynamic languages more because: * "double kilometerToMiles(double km) { return km / 1.6 }" here the types are of really low value, yet I have to type them in. * a mutable list of generic and variable arity event handlers. Really hard to specify as a type (most languages cannot do it). Really easy to use. * co- and contravariance and lists, the math work…

> * "double kilometerToMiles(double km) { return km / 1.6 }" here the types are of really low value, yet I have to type them in.

You shouldn't have to, and you wouldn't in say Haskell.

> a mutable list of generic and variable arity event handlers. Really hard to specify as a type (most languages cannot do it). Really easy to use.

You want the handlers to have types corresponding to the events they handle, right? I.e. a labelled product/coproduct (similar to HList). They do exist.

> * co- and contravariance and lists, the math works exactly opposite of intuition.

I don't understand the claim here?

> * when you change your mind on the types/arity beyond what your IDE can follow, it is a lot of low value work

In a well-designed language most of your functions will be generic, and the parts you have to change should only be the parts that your change actually affects. Obv. this ideal is not fully achieved yet, but we keep getting better at it.

> * if your test suite has 100% coverage of arguments/return-value and field usage, you have type checked your program.

Not true. That one example works for a given function does not prove the type is correct for all arguments. As a trivial example you could define a function like "def f(i) = if(i == 1000) "blah" else i". Typechecking would catch that immediately, but to catch it through testing you'd have to test every possible integer as input.

Re: Types

#80

Post by lmm »

one-more-minute wrote: post #78
lmm wrote: post #75

Earlier quoted context omitted.

It sounds very ad-hoc? (And Julia's benchmarking has not been reputable in the past, FWIW). > without the drawbacks (loss of interactivity, or inability to escape the type system when it's appropriate). One can absolutely have interactivity in a statically typed language, and virtually all statically typed languages support casting when you absolutely need to.

"Ad-hoc" seems subjective but to me it feels very carefully thought out. And while I've found the benchmarks to be accurate, I more importantly mean myself (and many others I know) being easily able to get high performance code when we need it. My second paragraph was only a personal take on what works for me, so YMMV, but nevertheless: I'm not arguing against static type systems in principle, but these are practical…

> "Ad-hoc" seems subjective but to me it feels very carefully thought out.

I guess I'd like to see a simple formalism.

> myself (and many others I know) being easily able to get high performance code when we need it.

That's true for a lot of languages. It doesn't make it Rust-level.

> I'm not arguing against static type systems in principle, but these are practical concerns rather than theoretical ones. I don't know of a mainstream static language that supports a fully dynamic REPL (Haskell's isn't great) and casting back and forth to `interface{}`, `Object`, or `Any` everywhere is a huge overhead compared to duck typing. I look forward to a future language solving those issues, but that's not the case today.

Shrug, not my experience. I don't know what you mean by "fully generic", but I've been very happy with the Scala REPL - I've never once thought "this would be easy in the Python REPL but I can't do it because of the type system". Casting is indeed a big overhead if you're doing it everywhere, but my experience is the cases where you need it are extremely rare.

Post reply on HN