Types • Hacker News Board

Re: Types

#161

Post by seanwilson » Wed, Aug 24, 2016, 11:42 PM UTC

tomp wrote: post #67

seanwilson wrote: post #11

Great overview article but I have a comment. > In Idris, we can say "the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument": > If we try to call this function as add 2 1, where the first argument is larger than the second, then the compiler will reject the program at compile time. > Haskell has no equivalent of the Idris type above, and Go has no e…

> Proving F matches the type is arbitrary hard and is impossible to automated in general So what? Even proving that array indices are not accessed out of bounds within loops would be a considerable leap in the state of the art of industrial programming languages. For most cases (i.e. linear integer arithmetics), that's always automatically (dis-)provable. We have to start somewhere...

> Even proving that array indices are not accessed out of bounds within loops would be a considerable leap in the state of the art of industrial programming languages. For most cases (i.e. linear integer arithmetics), that's always automatically (dis-)provable. We have to start somewhere...

It's a super interesting and important area, I was just pointing out it was a challenging one with lots of open issues.

Re: Types

#162

Post by seanwilson » Wed, Aug 24, 2016, 11:48 PM UTC

thinkpad20 wrote: post #108

seanwilson wrote: post #21

Earlier quoted context omitted.

> To some degree, you can choose what you want to prove about your algorithms in those languages. > It's perfectly possible to implement a sorting algorithm without proving that it actually sorts the input, or indeed returns a permutation of the input list at all. Sure, but my point is that any nontrivial property requires the programmer to write difficult formal mathematical proofs which is an activity completely un…

> Sure, but my point is that any nontrivial property requires the programmer to write difficult formal mathematical proofs which is an activity completely unlike what you see in mainstream strongly typed languages (e.g. Haskell, OCaml). So don't write the proofs then. Dependently typed languages don't require you to write proofs; they give you the ability to if you choose. Considering that it's impossible to write su…

> Considering that it's impossible to write such proofs in OCaml or Haskell, it seems strange to complain that they're hard to write in a dependently typed language.

My sole point is that when I see articles on here about dependently typed languages, the issue of how the proofs are generated and the challenges involved in doing this is overlooked almost every time. I think it's important these challenges are highlighted so people don't think dependent types are a magic wand that gives you safety with little effort.

Re: Types

#163

Post by eli_gottlieb » Wed, Aug 24, 2016, 11:53 PM UTC

catnaroek wrote: post #149

naasking wrote: post #148

Earlier quoted context omitted.

Hmm, I don't think you're being very charitable. That these programmers can write working programs suggest they sufficiently understand disjunction, conjunction, negation, conditionals and quantification. Perhaps they have trouble abstracting the semantics from their preferred language and/or syntax, but that doesn't mean they don't grasp their meaning.

I offer this thread as evidence: https://news.ycombinator.com/item?id=12342583

Hey, it's not the fault of the programming masses that some evil motherfucker conflated implementation extension (inheritance) and subtyping.

Subtyping = "A Inheritance = "A inherits B, if I try to actually use it as a B, it promises to work. However, it might actually blow up in my face, because it was keeping its extra details secret from me and promising they wouldn't blow up."

Re: Types

#164

Post by tel » Thu, Aug 25, 2016, 1:43 AM UTC

catnaroek wrote: post #130

tel wrote: post #113

Earlier quoted context omitted.

It's also simple enough to direct readers to note that types refer to expressions, not values. It's only through later evaluation relations do those expressions and their values end up sharing types.

Types can be seen both as collections of values and as collections of expressions. (I'm defining a “value” as “something the operational semantics of the language lets you substitute a variable with”.) In a call-by-value language, the former is embeddable in the latter. In a call-by-name or call-by-need language, the two coincide.

I disagree that it's a good idea to think of types as a "collection" (loosely) of values. It may be the case that you do not distinguish computation and value (here, I'm thinking of CBPV) but types only classify values as interpreted via their embedding into expressions.

Re: Types

#165

Post by acjohnson55 » Thu, Aug 25, 2016, 6:15 AM UTC

amelius wrote: post #82

> A type is a collection of possible values Ok, but do two collections with the same values always correspond to the same type?

Generally, no, at least with nominal typing.

Re: Types

#166

Post by acjohnson55 » Thu, Aug 25, 2016, 6:21 AM UTC

naasking wrote: post #87

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…

Formalism aside, it seems like it's most useful in practice to think of type as defining what can be done with a value. The sidesteps the idea of type being something permanent and inherent to a value. In practice, the type might be metadata discoverable and actionable at run-time, it might be something that exists at compile-time to determine correctness of a program (based on how values are used), or both.

Does this point of view leave out anything crucial?

Re: Types

#167

Post by mike_hearn » Thu, Aug 25, 2016, 8:08 AM UTC

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?

Maybe an analogy to a more mainstream language helps. I like using Kotlin these days:

http://kotlinlang.org/

which has nullable types. Imagine this code:

    fun useMessage(msg: Message) { .... }

    val s: Message? = someSocket.readNextMessage()   // Returns null if the socket has been closed.
    useMessage(s)

In Kotlin this would be a type error, the type of 's' is Message? and the question mark means it's possibly null. It won't compile. You can fix it by doing this:

    if (s != null) useMessage(s)

The act of testing 's' restricts its type inside the if block: we've proven it's not null, therefore the compiler will now accept this proof as evidence that the code is safe.

Idris isn't quite the same because it's a lot more general and the proofs are explicit instead of being implicit in the control flow: Idris types don't change when you test them, you get given a proof 'object' instead. But the basic idea is the same; your program does something that proves something about the type of a runtime value and that data can be used to improve program correctness.

Re: Types

#168

Post by catnaroek » Thu, Aug 25, 2016, 8:45 AM UTC

tel wrote: post #164

catnaroek wrote: post #130

Earlier quoted context omitted.

Types can be seen both as collections of values and as collections of expressions. (I'm defining a “value” as “something the operational semantics of the language lets you substitute a variable with”.) In a call-by-value language, the former is embeddable in the latter. In a call-by-name or call-by-need language, the two coincide.

I disagree that it's a good idea to think of types as a "collection" (loosely) of values. It may be the case that you do not distinguish computation and value (here, I'm thinking of CBPV) but types only classify values as interpreted via their embedding into expressions.

If a type couldn't be regarded as a collection of values in a strict language, then induction on datatypes would simply be unsound. Of course, induction on datatypes is unsound in Haskell, but it's sound in Standard ML.

Re: Types

#169

Post by lmm » Thu, Aug 25, 2016, 8:47 AM UTC

ozy wrote: post #114

lmm wrote: post #79

Earlier quoted context omitted.

> * "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.…

To most commenters: Indeed static typing has advantages as well, I just didn't list them. And some languages solve certain "complaints" I had. I would suggest though, that comparing haskell to javascript, is almost like comparing a train with an offroad bike. Which you choose when is a discussion at a whole different level. As for the list of event handlers example. The point it is a trivial piece of code. Any jQuery…

> The point it is a trivial piece of code. Any jQuery plugin writer can do it. Yet the type math behind it is complex. Java cannot express it. Most languages cannot be generic in function arity so cannot express it.

As the quote goes, dynamic typing is the belief that you can't explain to a computer why your code works, but you can keep track of it all in your head. If it's really hard to express in a given language then that's a problem with that language, but IME anything that's hard to express in statically-typed languages in general is a bad idea.

> And paying this penalty at API level, where ever user has to pay, is just a sin.

I'd say the opposite, because it's easy to cast away types when you don't need them, but it's virtually impossible to put type information back into a language that doesn't have it.

> The test suite idea was incorrect. Even 100% code coverage will not do. But for "normal" code, add reasonable amount of coverage. And any production runtime type error will be really surprising.

IME: For any given level of "I want all runtime errors to be at least this surprising", that level will be easier to achieve via types than via tests.

> A personal feeling on this topic is that it is all tradeoffs. But it makes me really happy to see gradual typing gaining traction. So you can start on your offroad bike, but end on a well oiled train, where that is worth the tradeoff. So you don't have to choose up front

IME it's ineffective - I spent years trying to get types working after the fact, but the trouble is that code that's 95% typechecked might as well be 0% typechecked. Every violation of typesafety needs to be visible right at the point where it happens if you're going to have any hope of correct code.

> Perhaps when we can even get runtime guarantees on perf/object layout when the type checker is happy.

That'd be nice. But it's going to take more advanced typing, not yes.

Re: Types

#170

Post by icen » Thu, Aug 25, 2016, 9:27 AM UTC

eximius wrote: post #139

So, how do these advanced types work? For their `add` example, I imagine just having x Also, I'm assuming the compiler has two classes of errors here: a counter example vs. unable to prove? Can anyone point me to documentation on these (in Idris, preferably)?

In Idris, there are functions `believe_me` and `really_believe_me`, which assert things to the compiler. They're generally only used for FFI code, or for extremely tedious proofs.

If you wanted to prove that a list was sorted, you'd write another datatype:

    IsSorted : Ord a => List a -> Type

which represents the proposition that the input list is sorted. You could encode this by requiring that any new element in the list is either the first element, or less than or equal to the previous element. Then, your sorting function could return a dependent pair:

    (l : List a ** IsSorted l)

which can be read as the list, accompanied by a proof that it is, in fact, sorted. Since your `IsSorted` type requires that the list is sorted, via construction, you won't be able to supply the output of the function unless your code is correct (or you use `believe_me`!).

The compiler doesn't generally come up with counterexamples for you; with this style, if the proof isn't complete, it won't compile.