Types • Hacker News Board

Re: Types

#131

Post by DanWaterworth » Wed, Aug 24, 2016, 5:31 PM UTC

AnimalMuppet wrote: post #126

DanWaterworth wrote: post #49

Earlier quoted context omitted.

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.

The question was, "how's that?". My answer was, it's possible for a small dependently typed language to be simpler than Haskell.

I'd already made the assertion that Idris was less complicated than Haskell.

Re: Types

#132

Post by naasking » Wed, Aug 24, 2016, 5:40 PM UTC

cwyers wrote: post #123

naasking wrote: post #119

Earlier quoted context omitted.

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

> And of what consquence is this purported "error" to the reader of this article?

Did you even read my comments? I already listed one falsehood that pervades our industry because types are misunderstand in exactly this way: "It's important not to perpetuate the false notion that sets of simple values suffice to explain types, because it entails the common and equally false notion that full test coverage in a dynamically typed language suffices to match the safety of a statically typed language."

This is blatantly, perniciously false, no doubt leading many people to choose dynamically typed languages to their detriment, yet this is what a reasonable person could conclude from the definitions in this article.

Finally, Newtonian physics governs every interaction an average person will have in their lifetime. The analogy that types-as-sets will suffice for nearly every interaction with types that a programmer will have in their lifetime is simply false. The fact that some programmers don't go beyond their first introduction to types makes a wrong definition almost dangerously false, given how much of our society is run by software.

Re: Types

#133

Post by chriswarbo » Wed, Aug 24, 2016, 5:50 PM UTC

naasking wrote: post #120

AnimalMuppet wrote: post #116

Earlier quoted context omitted.

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

Is it set-theoretic though? The article states:

> A type is a collection of possible values.

"Collection" doesn't necessarily imply "set"; perhaps the author chose this word on purpose to avoid such complaints? Would you also complain if a Web page giving an informal introduction to topology said "a space is a collection of points"? Keep in mind that in HoTT, types are spaces and points are values, and hence those two statements have similar meanings.

I know when I'm writing about technical topics, I often look for words which don't have a widely-used technical definition, since that frees me up to focus on what I want to talk about, rather than getting bogged down in the particulars of this-or-that preconceived notion. I could certainly imagine myself wanting to get across the idea of types "containing" values, and carefully choosing the word "collection" specifically to avoid the baggage associated with the word "set". Maybe the author did the same?

In such cases, I would much rather someone point out an existing field which is the same as what I describe ("Your idea of types as 'collections of values' sounds a lot like HoTT's idea that types are spaces of points"), rather than an existing field which is not what I describe yet uses a similar word ("Your use of the word 'collection' sounds a lot like 'set', which is a different theory without much relevance here")

Re: Types

#134

Post by catnaroek » Wed, Aug 24, 2016, 5:59 PM UTC

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…

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

The nice thing about this definition is that it reveals why reflection renders a type system useless: it destroys the type system's ability to enforce abstractions.

Re: Types

#135

Post by catnaroek » Wed, Aug 24, 2016, 6:04 PM UTC

naasking wrote: post #121

rntz wrote: post #118

Earlier quoted context omitted.

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

Under HoTT's take on propositions as “types where any two inhabitants are equal”, “types as propositions” is even less general than “types as sets”.

As I stated in a comment on that gist, what types denote varies from one type system to another: https://gist.github.com/garybernhardt/122909856b570c5c457a6c...

Re: Types

#136

Post by naasking » Wed, Aug 24, 2016, 6:06 PM UTC

chriswarbo wrote: post #133

naasking wrote: post #120

Earlier quoted context omitted.

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.

Is it set-theoretic though? The article states: > A type is a collection of possible values. "Collection" doesn't necessarily imply "set"; perhaps the author chose this word on purpose to avoid such complaints? Would you also complain if a Web page giving an informal introduction to topology said "a space is a collection of points"? Keep in mind that in HoTT, types are spaces and points are values, and hence those tw…

> "Collection" doesn't necessarily imply "set"; perhaps the author chose this word on purpose to avoid such complaints?

I think it's still wrong, but let's get concrete in the more unusual type systems to check. What is the "collection of values" for a type in TyPiCal [1]?

What is the "collection of values" for substructural types, like linear types [2] or affine types [3]?

I don't think "collection", set-based or otherwise, can capture these types.

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

[2] https://www.cs.cmu.edu/~fp/courses/linear/handouts/lintt.pdf

[3] http://users.eecs.northwestern.edu/~jesse/pubs/alms/tovpucel...

Re: Types

#137

Post by munificent » Wed, Aug 24, 2016, 6:15 PM 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?

Yes, they do.

Re: Types

#138

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

catnaroek wrote: post #135

naasking wrote: post #121

Earlier quoted context omitted.

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

Under HoTT's take on propositions as “types where any two inhabitants are equal”, “types as propositions” is even less general than “types as sets”. As I stated in a comment on that gist, what types denote varies from one type system to another: https://gist.github.com/garybernhardt/122909856b570c5c457a6c...

No one except mathematicians and type theorists are using HoTT, where every programmer in existence is using first-order and sometimes second-order logic. I think it should be obvious which is more appropriate if this is supposed to be an introduction.

The idea that types express propositions in first- or second-order logic about a program one is writing is sufficiently general for every programmer to understand the proper scope of type checking. Types-as-sets is simply false as an introductory concept.

Re: Types

#139

Post by eximius » Wed, Aug 24, 2016, 6:37 PM UTC

So, how do these advanced types work?

For their `add` example, I imagine just having xAlso, 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)?

Re: Types

#140

Post by catnaroek » Wed, Aug 24, 2016, 6:51 PM UTC

naasking wrote: post #138

catnaroek wrote: post #135

Earlier quoted context omitted.

Under HoTT's take on propositions as “types where any two inhabitants are equal”, “types as propositions” is even less general than “types as sets”. As I stated in a comment on that gist, what types denote varies from one type system to another: https://gist.github.com/garybernhardt/122909856b570c5c457a6c...

No one except mathematicians and type theorists are using HoTT, where every programmer in existence is using first-order and sometimes second-order logic. I think it should be obvious which is more appropriate if this is supposed to be an introduction. The idea that types express propositions in first- or second-order logic about a program one is writing is sufficiently general for every programmer to understand the…

> No one except mathematicians and type theorists are using HoTT,

Right.

> where every programmer in existence is using first-order and sometimes second-order logic.

I'm not so sure about this one. Perhaps by “programmer” you mean “every Haskell programmer”? Even then I'm still not sure. Are you counting “let's approximate `forall x. P(x)` with the large but finite conjunction `P(a) /\ P(b) /\ P(c) ...`” as “using first-order logic”?