Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The Little Typer

mitpress.mit.edu

Post reply on HN
Print view View original

121–130 of 138 posts

Re: The Little Typer

#121

Post by jedharris »

Several comments elaborate on the big gap between normal programming practice (e.g. structurally recursive algorithms) and the great difficulty of dependent typing those practices. Some of these comment on how dependent types are "just out of the lab".

This brings into focus a question I've had for a long time: Why this gap, and especially in this direction? E.g. in aerodynamics we had Bernoulli's principle for a couple of hundred years before we could build airplanes, which depend on it. In formal language theory we had lambda calculus, Turing's universality results, etc. decades before we had Lisp and Fortran.

We often see the difficulty of building a practice to exploit theory.

So it seems very strange to me that we are able to write / plug together literally world-spanning software systems -- which do have bugs but fact work correctly nearly all the time. But we can't easily well-type even simple algorithms with extremely well understood properties.

Why this huge gap, in this direction?

Re: The Little Typer

#122

Post by KirinDave »

jedharris wrote: post #121

Several comments elaborate on the big gap between normal programming practice (e.g. structurally recursive algorithms) and the great difficulty of dependent typing those practices. Some of these comment on how dependent types are "just out of the lab". This brings into focus a question I've had for a long time: Why this gap, and especially in this direction? E.g. in aerodynamics we had Bernoulli's principle for a cou…

I'd argue that there aren't many "simple" programs with "well-understood" properties in use in industry.

Software is a bit different from architecture in that partial failures tend to work and can be refined around repeatedly (a partially failed building tends to rip itself apart, partial failures in software can linger for years and only cease when their dependencies fault out). People are just more amenable to altering their processes, products and lives around bad software.

I think dependent typing reveals to us, to some extent, what a house of cards we truly have built for ourselves.

Re: The Little Typer

#123

Post by jedharris »

KirinDave wrote: post #122
jedharris wrote: post #121

Several comments elaborate on the big gap between normal programming practice (e.g. structurally recursive algorithms) and the great difficulty of dependent typing those practices. Some of these comment on how dependent types are "just out of the lab". This brings into focus a question I've had for a long time: Why this gap, and especially in this direction? E.g. in aerodynamics we had Bernoulli's principle for a cou…

I'd argue that there aren't many "simple" programs with "well-understood" properties in use in industry. Software is a bit different from architecture in that partial failures tend to work and can be refined around repeatedly (a partially failed building tends to rip itself apart, partial failures in software can linger for years and only cease when their dependencies fault out). People are just more amenable to alte…

Several interesting points but maybe they show something different from what you intend.

Network stacks, databases etc. that correctly handle trillions of interactions, some of them adversarial, have indeed been "refined around [their failures] repeatedly" and have gotten pretty robust along the way.

On the other hand useful formal accounts of their behavior (distributed, highly parallel, loosely coupled, asynchronous) seem far, far way.

It would be helpful to have an account of approximation to formal properties, especially if that can help us understand how repair and refactoring can lead to progressively better approximations.

Perhaps the house of cards that is revealed is formal methods not software.

Re: The Little Typer

#124

Post by KirinDave »

jedharris wrote: post #123
KirinDave wrote: post #122

Earlier quoted context omitted.

I'd argue that there aren't many "simple" programs with "well-understood" properties in use in industry. Software is a bit different from architecture in that partial failures tend to work and can be refined around repeatedly (a partially failed building tends to rip itself apart, partial failures in software can linger for years and only cease when their dependencies fault out). People are just more amenable to alte…

Several interesting points but maybe they show something different from what you intend. Network stacks, databases etc. that correctly handle trillions of interactions, some of them adversarial, have indeed been "refined around [their failures] repeatedly" and have gotten pretty robust along the way. On the other hand useful formal accounts of their behavior (distributed, highly parallel, loosely coupled, asynchronou…

> Network stacks, databases etc. that correctly handle trillions of interactions,

But they have also incorrectly handled a similar order of magnitude of transactions! Routing failures and issues that people troubleshoot around, misconfigurations and bugs, and simple electromechanical glitches exist in the real world and they're not some kind of zebra, you can force them by pining a server.

Our networking systems "mostly work" because they're persistent, and because (interestingly) the difference between a perfectly coordinated networking system and a purely chaotic networking system with random traffic is actually rather small compared to other domains.

> On the other hand useful formal accounts of their behavior (distributed, highly parallel, loosely coupled, asynchronous) seem far, far way.

Generally what makes a difference between a "robust" program and a brittle program that simply falls over is how much of its own failure it attempts to take into account. Even bad models of self-failure (pre-OTP erlang, for example) are better than no model at all.

> Perhaps the house of cards that is revealed is formal methods not software.

Given that almost no one applies formal methods and dependent typing is by no means a part of that discipline, I'm not sure it's fair to draw those comparisons in this conversation.

Dependent Typing is not formal methods, nor is it verifcation. It's code that allows for automated reasoning. It's closer to the machinery of formal methods, like datalog or an SMT solver.

Re: The Little Typer

#125

Post by jedharris »

KirinDave wrote: post #124
jedharris wrote: post #123

Earlier quoted context omitted.

Several interesting points but maybe they show something different from what you intend. Network stacks, databases etc. that correctly handle trillions of interactions, some of them adversarial, have indeed been "refined around [their failures] repeatedly" and have gotten pretty robust along the way. On the other hand useful formal accounts of their behavior (distributed, highly parallel, loosely coupled, asynchronou…

> Network stacks, databases etc. that correctly handle trillions of interactions, But they have also incorrectly handled a similar order of magnitude of transactions! Routing failures and issues that people troubleshoot around, misconfigurations and bugs, and simple electromechanical glitches exist in the real world and they're not some kind of zebra, you can force them by pining a server. Our networking systems "mos…

Again lots of interesting points. Only time for one response.

You highlight networking but I also mentioned databases. Schematizing your comment "Our... systems "mostly work" because... the difference between a perfectly coordinated... system and a purely chaotic... system... is actually rather small".

I think banks and customers would disagree rather violently regarding the (distributed, asynchronous) system that handles credit card transactions.

And yet this system is certainly subject to a lot of attacks, not just random errors.

Re: The Little Typer

#126

Post by etatoby »

bjz_ wrote: post #109
etatoby wrote: post #104

Earlier quoted context omitted.

I recommend these introductory lectures to Category Theory. I'm going through them right now. I assume you know some math/set theory and some Haskell, otherwise you may want to work though some of the chapters in Real World Haskell first. Oh and put the videos at 1.25× or 1.5× otherwise you will fall asleep. https://www.youtube.com/user/DrBartosz

Don't get me wrong - CT is a super handy thing to learn, and it pops up a ton when thinking about any software, including type checkers and compilers, but the OP was specifically asking about type theory and programming language implementation. Yes, you can express lots of category theory in terms of type theory (the dream is to implement all of it in terms of TT so that we can mechanise it), but it won't be the best…

I probably phrased my suggestion wrong. Yes, it's not central to OP's enquiry. But I did find a basic understanding of CT to help a lot when reasoning about types, and that lecture series gives just that in a relatively simple way.

Re: The Little Typer

#128

Post by sn9 »

a_imho wrote: post #100
rdc12 wrote: post #92

Earlier quoted context omitted.

The worlds population living on $10/day, will have no use for a book on a niche aspect of type systems. The majority of people on that wage will probably not even access to a computer.

An obvious counterexample is students.

They can request that their library pick up a copy. Or get an inter-library loan.

Re: The Little Typer

#129

Post by ernst_klim »

KirinDave wrote: post #116
bbeonx wrote: post #12

Earlier quoted context omitted.

My guess is because OP has been burned by the "LEARN THIS NEW THING, IT'S REALLY COOL AND POWERFUL AND ALL OF THE COOL KIDS ARE DOING IT (and oh by the way many of the simple things you do all the time are incredibly inconvenient...)" narrative one too many times. Adopting something purely on it's merits is a bad idea, but nobody ever writes the book about a language/paradigm's downsides. I'm pretty sure that was the…

It's not even really possible to "adopt" dependent typing today. It's only emerged from the realm of academic curiosity and only two implementations exist that are anywhere near "practical" in the context you're describing. Both of those implementations are very honest about their shortcomings, and nearly every talk and blogpost for them mentions you can't yet use this in many industrial contexts. It's very difficult…

>only two implementations exist that are anywhere near "practical"

Out of curiosity, why F* or Idris are not practical?

Re: The Little Typer

#130

Post by bjz_ »

etatoby wrote: post #126
bjz_ wrote: post #109

Earlier quoted context omitted.

Don't get me wrong - CT is a super handy thing to learn, and it pops up a ton when thinking about any software, including type checkers and compilers, but the OP was specifically asking about type theory and programming language implementation. Yes, you can express lots of category theory in terms of type theory (the dream is to implement all of it in terms of TT so that we can mechanise it), but it won't be the best…

I probably phrased my suggestion wrong. Yes, it's not central to OP's enquiry. But I did find a basic understanding of CT to help a lot when reasoning about types, and that lecture series gives just that in a relatively simple way.

Fair enough! Yeah, I've heard good things about that series.
Post reply on HN