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

121–130 of 198 posts

Re: Types

#121

Post by naasking »

rntz wrote: post #118
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 logi…

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

Right, I wasn't advancing the propositional definition as the only one, merely as one that sufficiently captures the generality, because the article's current definition of types-as-sets is insufficiently general.

Re: Types

#122

Post by levbrie »

dochtman wrote: post #93
levbrie wrote: post #92

Kind of shocked nobody mentioned this, even if it is a bit of an aside, but umm, I've been dying for anything at all from Gary Bernhardt - I don't even know what to say except that it makes me hope however unrealistically that will one day get something like the magnum opus that is "Destroy All Software" from him again.

You know he just started to post new stuff, right? https://www.destroyallsoftware.com/screencasts/catalog

I know. Mind blown.

Re: Types

#123

Post by cwyers »

naasking wrote: post #119
cwyers wrote: post #117

Earlier quoted context omitted.

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

And of what consquence is this purported "error" to the reader of this article? Would you edit a children's book about zoo animals from "This is a lion" to "This is a photograph of a lion printed onto paper?" What pedagogic purpose does your correction serve?

We teach Newton's physics to children (and even many adults) even though they've been supplanted by later theories, not because we don't know what the correct answer is, but because Newtonian physics are much easier to grasp and because they still give a useful view of the world around us, even if they break down in the extremes. Why is this any different?

Re: Types

#124

Post by ozy »

spriggan3 wrote: post #83
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…

> Test suits shouldn't be about checking if a return value is of expected type

Indeed and so they don't have to. When you have reasonable code coverage, it is really surprising to encounter type issues in production. And they are the easiest mistakes to fix. But the point is, runtime checks happen implicitly as you run the code. So no "implementing a type checker" needed ...

On the other hand my comment on when you get the equivalent of being fully type checked was incorrect. Even 100% code coverage will not guarantee it for some code.

I like both kind of languages, and use both. While you get some advantages in static languages, you do also pay a price in language semantics and effort. It is good to point that out, so we can continue making progress, like Crystal or latest C# (and latest F#!). There used to be a time when the mood was: Java is good for all, stop confusing us with your new languages.

Re: Types

#125

Post by AnimalMuppet »

DSMan195276 wrote: post #112
naasking wrote: post #89

Earlier quoted context omitted.

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

In theory, languages have type systems. In practice, compilers do.

If there's more than one C compiler, and they behave differently on this, then in practice, C has more than one type system.

Re: Types

#126

Post by AnimalMuppet »

DanWaterworth wrote: post #49
tome wrote: post #45

Earlier quoted context omitted.

> Type checking Idris is much simpler than Haskell. Is it? How's that?

Haskell's type system has accrued complexity over the years, whereas a small dependently typed language can be implemented very easily [1]. [1] https://www.andres-loeh.de/LambdaPi/

That's not a fair comparison, though. A fair comparison might be Haskell's type system compared to Idris, or a small dependent typed language against a small type inference language.

Re: Types

#127

Post by AnimalMuppet »

NhanH wrote: post #15

The article is mainly focused on static typing. I guess it makes sense since the title is "Types". Although reading this, you might just think that dynamic typing is good for nothing. The more practical part of the article is great. However, the theoretical part could use some works. Especially the terminology isn't actually clear. Takes some example, what is "memory-safe" ? The only example makes it sounds like boun…

> And what does "no way to escape the language's type rules" mean?

I can give you an example, from bitter experience.

In the original Pascal, the size of an array was part of the type of an array. There was no possible type for a variable-sized array. And you couldn't cast from an array of one fixed size to an array of another fixed size.

Well, we were trying to do a 2D numerical simulation on a grid, with the size of the grid being user-specified. The original version of the program used a linked list to simulate the array, since you could have an arbitrarily-long linked list. But this meant that, if the simulation was 60x60, to reference the cell directly below the current one, you had to follow 60 links to get there!

I replaced it with a 2D array of a fixed size, with the size being the largest amount we could fit into available memory (it was on an embedded system, so the amount of memory available was predictable). Of that, we used only the user-specified subset to do the simulation.

TL;DR: If you need to do something that's outside what's allowed by your type system, and there's no way to escape the language's type system, you're trapped.

Re: Types

#128

Post by paulddraper »

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?

Yes, but if remember you can always say that the values are different.

A blue 5, and a red 5.

Five feet, or five inches.

Re: Types

#129

Post by paulddraper »

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.

The cost of non-Java-style types is compile time :)

Re: Types

#130

Post by catnaroek »

tel wrote: post #113
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…

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.
Post reply on HN