Types • Hacker News Board

Re: Types

#111

Post by [deleted] » Wed, Aug 24, 2016, 3:46 PM UTC

mietek wrote: post #104

catnaroek wrote: post #62

Earlier quoted context omitted.

I'm not comparing dependent types vs. no dependent types. I'm comparing higher-order dependent types (Agda, Idris, Coq, etc.) vs. first-order dependent types: https://news.ycombinator.com/item?id=12350147 Seriously, Coq-style proof scripts are utterly unredable when they grow past a certain size. The only way to understand them is to replay them, so that you can see the intermediate hypotheses and goals.

I agree. Note that the Coq-style tactics-based approach is not the only possibility. In Agda, you are expected to write proofs in a functional style, similar to Haskell programs. There is a small amount of integrated automation, which helps you fill in holes in your proofs — however, the results are explicit proof terms, inserted at the right place in your program. Systems which behave in this fashion have the de Bru…

[deleted]

Re: Types

#112

Post by DSMan195276 » Wed, Aug 24, 2016, 3:53 PM UTC

naasking wrote: post #89

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

The issue with that idea is that there is more than one C compiler. Some of them issue no warnings at all, and some of them (like `gcc`) will yell at you and probably break your code if you attempt to do some of the things I outlined.

I disagree with saying it is 'allowed' by the type system, because a smart C compiler could throw out your code and refuse to compile it if you do such things, and in doing so would still be within the C standard. Some work has already been done on this front in `gcc` (And I would assume `clang`) - the issue tends to be that by doing this, you end-up breaking some older code that used to work fine. And since older compilers didn't enforce these rules, people aren't as aware of them.

Re: Types

#113

Post by tel » Wed, Aug 24, 2016, 4:06 PM UTC

naasking wrote: post #109

chriswarbo wrote: post #98

Earlier quoted context omitted.

Well, there are several ways to think about types, especially regarding this article, which tries to cover static and dynamic types. Most formal definitions/treatments of types I've come across do not apply to dynamic types at all; usually the typing formalism says nothing about dynamically typed programs/values other than giving them one big recursive type. What we would informally call "dynamic types" are then trea…

> While such distinctions are certainly useful, an introductory/broad-overview explanation like this seems to benefit without such complications/distractions. I don't think misrepresenting types is the way to go. An introduction like I just gave seems simple enough, where a type is a proposition about a program, and you just then explain that most such propositions are "variable X may take on values from set Y". It's…

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.

Re: Types

#114

Post by ozy » Wed, Aug 24, 2016, 4:09 PM UTC

lmm wrote: post #79

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

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 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. Spending time on it is not worth the trouble. And paying this penalty at API level, where ever user has to pay, is just a sin.

Some discussion from the dartlang on covariant lists: https://www.dartlang.org/articles/design-decisions/why-dart-...

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. And even when it does happen, the fix is clear and quick.

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. Perhaps when we can even get runtime guarantees on perf/object layout when the type checker is happy.

Re: Types

#115

Post by zeveb » Wed, Aug 24, 2016, 4:12 PM UTC

> The unsatisfying solution used in practice is to give eval() the type Any, which is like Object in some OO languages or interface {} in Go: it's the type that can have any value. Values of type Any aren't constrained in any way, so this effectively removes the type system's ability to help us with code involving eval. Languages with both eval and a type system have to abandon type safety whenever eval is used.

It's not quite true that they must abandon type safety: rather, they must abandon a certain kind of compile-time type check. It's not unsafe to use eval or Any values (i.e., it won't crash the system); one must simply examine the Any value (at runtime, natch) and do stuff with it.

Re: Types

#116

Post by AnimalMuppet » Wed, Aug 24, 2016, 4:16 PM UTC

naasking wrote: post #109

chriswarbo wrote: post #98

Earlier quoted context omitted.

Well, there are several ways to think about types, especially regarding this article, which tries to cover static and dynamic types. Most formal definitions/treatments of types I've come across do not apply to dynamic types at all; usually the typing formalism says nothing about dynamically typed programs/values other than giving them one big recursive type. What we would informally call "dynamic types" are then trea…

> While such distinctions are certainly useful, an introductory/broad-overview explanation like this seems to benefit without such complications/distractions. I don't think misrepresenting types is the way to go. An introduction like I just gave seems simple enough, where a type is a proposition about a program, and you just then explain that most such propositions are "variable X may take on values from set Y". It's…

> > There are several ways to think about types.

> I don't think misrepresenting types is the way to go. An introduction like I just gave seems simple enough, where a type is a proposition about a program...

chriswarbo's point is: That's one way to think about types. It's not the only way, or even the only valid way. If you're going to disagree with chriswarbo, simply ignoring his/her point and reiterating your own isn't a good way to do it.

Can you demonstrate that your definition is the only valid way to think about types? Can you demonstrate that all other ways are subsets of your way? Those would be useful replies that would actually answer chriswarbo.

Re: Types

#117

Post by cwyers » Wed, Aug 24, 2016, 4:16 PM UTC

naasking wrote: post #109

chriswarbo wrote: post #98

Earlier quoted context omitted.

Well, there are several ways to think about types, especially regarding this article, which tries to cover static and dynamic types. Most formal definitions/treatments of types I've come across do not apply to dynamic types at all; usually the typing formalism says nothing about dynamically typed programs/values other than giving them one big recursive type. What we would informally call "dynamic types" are then trea…

> While such distinctions are certainly useful, an introductory/broad-overview explanation like this seems to benefit without such complications/distractions. I don't think misrepresenting types is the way to go. An introduction like I just gave seems simple enough, where a type is a proposition about a program, and you just then explain that most such propositions are "variable X may take on values from set Y". It's…

> An introduction like I just gave seems simple enough

Simple enough for what?

And I don't see why a bit of pedantry about Haskell's type system requires rewriting an introduction that's expressive and actually simple, not just "simple enough" from a certain point of view.

Re: Types

#118

Post by rntz » Wed, Aug 24, 2016, 4:18 PM 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…

(Static) types may be seen as propositions, but this is just one interpretation of them. We can also interpret types as sets (although this doesn't work out very well except in very simple languages), as domains (most commonly), as cpos, as relations over closed terms (PERs), and so forth.

The types-as-propositions interpretation is a particularly useful one because it lets us take ideas from the field of formal logic and apply them to programming. But it is only one interpretation, and not a definition of what types are.

I don't think it's possible to give "type" a good, short definition. For me John Reynolds' definition comes closest: "Type structure is a syntactic discipline for enforcing levels of abstraction." But that's rather a mouthful, and not a good introduction to what types are.

> A type is a proposition, and "This binding has one of these possible values" is merely one type of proposition.

The type that an expression or variable has does not correspond to the proposition that that expression has a certain set of possible values! You're mixing the object-level (the language & its types) with the meta-level (assertions about the language). This is a total misunderstanding of Curry-Howard. Rather, the values an expression might take on can be interpreted as proofs of the corresponding proposition.

Re: Types

#119

Post by naasking » Wed, Aug 24, 2016, 4:20 PM UTC

cwyers wrote: post #117

naasking wrote: post #109

Earlier quoted context omitted.

> While such distinctions are certainly useful, an introductory/broad-overview explanation like this seems to benefit without such complications/distractions. I don't think misrepresenting types is the way to go. An introduction like I just gave seems simple enough, where a type is a proposition about a program, and you just then explain that most such propositions are "variable X may take on values from set Y". It's…

> An introduction like I just gave seems simple enough Simple enough for what? And I don't see why a bit of pedantry about Haskell's type system requires rewriting an introduction that's expressive and actually simple, not just "simple enough" from a certain point of view.

It's not pedantry, it's a basic definition. There are plenty of languages with stronger type properties that can't be captured by types-as-sets. While the current introduction may be simple, it's also wrong.

Re: Types

#120

Post by naasking » Wed, Aug 24, 2016, 4:22 PM UTC

AnimalMuppet wrote: post #116

naasking wrote: post #109

Earlier quoted context omitted.

> While such distinctions are certainly useful, an introductory/broad-overview explanation like this seems to benefit without such complications/distractions. I don't think misrepresenting types is the way to go. An introduction like I just gave seems simple enough, where a type is a proposition about a program, and you just then explain that most such propositions are "variable X may take on values from set Y". It's…

> > There are several ways to think about types. > I don't think misrepresenting types is the way to go. An introduction like I just gave seems simple enough, where a type is a proposition about a program... chriswarbo's point is: That's one way to think about types. It's not the only way, or even the only valid way. If you're going to disagree with chriswarbo, simply ignoring his/her point and reiterating your own i…

I never claimed it was the only valid definition, but the current set-theoretic definition is simply wrong. The propositional definition is at least right (and fairly common), and isomorphic to other definitions.