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

81–90 of 198 posts

Re: Types

#81

Post by kilotaras »

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 }

But what if you could have `miles kilometersToMiles(kilometers km)`? Under the hood its the same old doubles but you would be able to catch errors such as the one that caused Surveyor failure [1].

e.g. Haskell has units[2] and dimensional[3] that allow you to do exactly that

[1] https://en.wikipedia.org/wiki/Mars_Climate_Orbiter#Cause_of_...

[2] https://github.com/goldfirere/units

[3] https://github.com/bjornbm/dimensional

Re: Types

#82

Post by amelius »

> A type is a collection of possible values

Ok, but do two collections with the same values always correspond to the same type?

Re: Types

#83

Post by spriggan3 »

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…

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

The most horrible argument in favor dynamic typing in my opinion. Test suits shouldn't be about checking if a return value is of expected type, that's ridiculous. It's implementing a type checker manually.

There are a lot of things statically typed languages can do to make types painless :

- (global) type inference (Crystal does that)

- co and contravariance, it is not limited to dynamically typed language

- optional parameters

- adhoc type declaration like in C# (ex {x:1,y:"a"} is a type).

- contracts

- pattern matching

- generics

- ect ... etc ...

I just dislike dynamically typed languages. Even interpreted languages should be statically typed IMHO. Again, there are multiple ways to make statically typed language painless when it comes to types.

Re: Types

#84

Post by bjz_ »

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…

What do you feel is lacking from Haskell's REPL?

Re: Types

#85

Post by bjz_ »

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 found Idris pretty easy to get started with - that's part of it's goal, making dependent types easier to get started with. From there I think it would be easier to go to Agda or Coq, but I haven't explored much there myself.

Re: Types

#86

Post by bo1024 »

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?

You can't because the function takes three arguments: an x and y of type integer, and a "z" of type "proof that x This is the "types as propositions, proofs as instances" Curry-Howard correspondence lightbulb: The type "x < y" is a proposition, and if you can find any z at all of that type, then z is a proof of the proposition. So by passing in such a z that has been verified to have that type, you've certified that x < y.

Re: Types

#87

Post by naasking »

Decent overview of many concepts, but the opening line isn't strictly true:

> A type is a collection of possible values.

A type is a proposition, and "This binding has one of these possible values" is merely one type of proposition. So a type is much more powerful than a simple set-based interpretation, even though this is how most people think about it.

For instance, in Haskell you can encode a region calculus that ensures prompt reclamation of file handles and other scarce resources [1]. The relations between nested regions to ensure correctness seems awkward to interpret as a set, but it's straightforward if you just think of types as a relation.

[1] http://okmij.org/ftp/Haskell/regions.html#light-weight

Re: Types

#88

Post by naasking »

catnaroek wrote: post #33
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.

I'd love to give more concrete examples, but I'm slightly hampered by the fact the type system I want isn't actually implemented anywhere. I have a rough sketch of the design of the type system I want, and I've been looking for a computer scientist, logician or mathematician to help me polish the design and prove that it is, in fact, type safe. But I couldn't find anyone. :-|

Why not just learn Coq or Agda yourself? There are also sorts of introductions for simple type systems that I'm sure you can build off of.

Re: Types

#89

Post by naasking »

DSMan195276 wrote: post #30

Being someone who enjoys C (Though I readily admit the type system is generally weak compared to the others on the list) there's a little misinformation on this page that I think it worth clearing up - though I think the majority of the information is still perfectly good: C does not 'allow' you to do a lot of the things mentioned on this page, it just doesn't generally carry around all the information to check and m…

Since this articles is about types, any behaviour the compiler doesn't check or doesn't generate a type error is "allowed".

Re: Types

#90

Post by naasking »

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…

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

This is absolutely false. Others have pointed this out, but types are much more general than runtime checks in dynamically typed languages. For instance, you can check at compile-time that your program doesn't have data races or deadlocks:

http://www-kb.is.s.u-tokyo.ac.jp/~koba/typical/

Or design a library in Haskell to ensure file handles and other scarce resources are promptly reclaimed:

http://okmij.org/ftp/Haskell/regions.html#light-weight

Neither of these are testable in dynamically typed languages. Static types are much more powerful than dynamic types, in general.

Post reply on HN