joel_ms

> That passes the type checker just fine.

I think you are running into some weird haskellisms with your Bottom-type.

The normal way of defining that in haskell is using the "EmptyDataDecls" pragma, like this:

    {-# LANGUAGE EmptyDataDecls #-}

    data Empty 

    g :: Empty -> a
    g x = x 

Which doesn't pass the type checker.

(From a theoretic standpoint, I would have thought your Bottom was a essentially a type-level identity function..)

No‚ it's not. They're not attacking the validity of your statement by criticizing your tone, they are criticizing the effectiveness of your communication. And tone is completely relevant in that context.

I think weakening herd immunity and resurrecting deadly diseases in areas where they were previously erradicated puts them in the 'harmful conspiracy' category.

When those highly connected CEOs sit on the boards of eachothers companies and determine eachother's sallaries, "what someone else is willing to pay" is not an independent variable.

"People of the same trade seldom meet together, even for merriment and diversion, but the conversation ends in a conspiracy against the public, or in some contrivance to raise prices."

— Adam Smith, The Wealth of Nations, 1776

> Yes, static analysis is very useful for understanding what the source code will do for inputs you didn't test. Testing is rarely exhaustive. However, testing will find performance issues where static analysis won't.

Static analysis is a funny word to use about what Agda does.. Remember, Agda has dependent types, so what you're calling "static anaysis" involves evaluating/executing functions. In fact it needs to be able to evaluate/execute any functions beyond value-level in any imported modules just to be able to parse a sourcefile, due to the presence of mixfix-notation[0] and how it affects typechecking.

> Testing is rarely exhaustive. However, testing will find performance issues where static analysis won't.

How do you test a function that takes a natural number? Not an unsigned integer, but an actual countably infinite natual number? For every natural number n you test your function with, you can construct a new natural number n+1 which your function is untested for, (literally) ad infinitum.

The answer, of course, is mathematical induction[1] and in the case of more general data structures we have the more general structural Induction[2]. But at this point you don't call it testing, you call it proving, and it's this that Agda is aspiring to.

> To quibble with "none of these are acceptable in Agda": it seems unlikely that Agda or anything like it would detect hangs or timeouts due to code not meeting its deadline.

Yes, your right that actually detecting hangs or timeouts would be difficult or impossible. But that's not what Agda does. Agda only allows functions that the compiler can figure out are total, which can never be all total functions (otherwise we would have a solution to the halting problem I think.)

Basically, functions are either (provably total by the compiler) and hence acceptable. In the case of long/diverging computations Agda just has a timeout threshold, where it rejects a function if it takes too long to evaluate it during typechecking. I'm pretty sure that's what would happen if you tried "a ↑↑↑ b".

> Of course, as a another commenter pointed out, this sort of practical bug-finding is not actually what the termination guarantee is for.

Correct, it's not for bug-finding at all, but rather to keep the type theory/logic sound when using Agda as a proof assistant.

Just to be clear: your criticism makes a lot of sense from a software engineering perspective, but considering the general performance characteristics of Agda, and the almost noneexisiting tooling around it, I think we're a couple of years away from "deployment specific assumtions" being something Agda needs to be too concerned about :)

[0] You can define a function "if_then_else_" where the underscores represent arguments, so you would use it like this: "if TRUTH_VALUE then TRUE_CONSEQUENCE else FALSE_CONSEQENCE"

[1] https://en.wikipedia.org/wiki/Mathematical_induction

[2] https://en.wikipedia.org/wiki/Structural_induction

>I don't think it comes up much in practice because bugs due to non-terminating code don't actually happen much to begin with (compared to all bugs that cause hangs or timeouts), and when they do they are often found via testing. We know that a function terminates for any inputs it was tested with.

None of these are acceptable in Agda actually, since they would all be partial functions (i.e. functions that are not defined for some inputs.) The simplest, intuitive explanation is that since Agda has dependent types it needs to be able to evaluate functions during typechecking, and if you allow partial functions (e.g. infinite loops, halting functions, functions that timeout, or functions that are undefined for untested input) the typechecking would be undecidable.

Instead Agda has a bunch of built-in tools to help the compiler figure out if a function is total (the opposite of a partial function, meaning it's defined for all possible inputs). Things like the termination checker can detect a subset of all terminating functions, and sized types let the programmer aid the compiler in figuring this out. There are also language pragmas to overide this totality check on a per function basis.

I've implemented an algorithm, that I knew on paper terminated, and had it rejected by Agda, although I'm not experienced enough to know how easily these things are solved in general.

> What's not so easy to understand for an imperative programmer is this: Why should I jump through those hoops just to have a readonly structure? Why not just, you know, program imperatively?

Beacuse imperative programs are rife with "statements". Opaque lines of code that may or may not do something, somewhere, which cannot be manipulated as first class objects.

Why would you ever wanna program with that weird restriction?

And yet MLTT led to Coq, Agda, Idris and Lean, while your ”PL practice” approach sounds like it would lead to, well, Go.

It’s a ”function value”, since you haven’t applied it to another expression.

Whether that is a partially or fully applied function doesn’t matter in the first syntax, but in the second syntax you have to add ugly parens to disambiguate the partially applied function from the function call.

As soon as you get serious about type-level functions, the first syntax beats the shit outta the second.

(Edit: The citation got messed up, it should be:

>The only thing you can do with a function is call it.

You can also abstract over it, and pass it around. Which allows you to build whatever you want, numbers, booleans, if-then-else, etc.)

> if everything is a function, then it's all a big ball of mud.

Not really, each distinct function will still have a distinct type. (This is largely why I prefer ml-family languages over lisps)

>The only thing you can do with a function is call it. You can also abstract over it, and pass it around. Which allows you to build whatever you want, numbers, booleans, if-then-else, etc.

The combination of function as your basic unit of abstraction and types as the differentiating descriptor is kind of the opposite of a mess, as you have a correspondence to familiar logic operations.

A function type A -> B is implication (given A, we have B), a product type (A,B) is conjuction (A and B), a sum type A|B is disjunction (A or B). (Sure, the logic isn’t necessarily sound, but it’s still useful).

When you have the fundamentals down you can build whatever capability system you need on top of solid abstractions.

I’m currently working on an ETL-project in haskell and it’s structured around a similar capabilities divide as you describe, defined by typeclasses/interfaces, it’s just all functions.

They’re not the same expression though. The first gets defaulted to Integer, the second is specialized to Int by the (!!) function. (Integer is unbounded, Int is bounded)

The rest of your argument is fairly vague and unspecific. But I would suggest trying to understand the underlying type theory instead of focusing on the affordances that the type system makes for practicality and usability concerns. In my experience that makes it a lot clearer why the type inference works the ways it does in some of the weird cases. (That’s not to say that Haskell doesn’t have it’s warts..)

Are you sure about Haskell not having m:n threads? Because it's seems weird, considering GHC is listed as one of a few examples on wikipedia: https://en.m.wikipedia.org/wiki/Thread_(computing)#M:N_.28hy...

>A program written by a developer and used by a user is a relationship between that developer and the user.

What about the relationship between you/Mozilla and the firefox users? This thread is evidence that at least some of the users are not happy that you are (in their eyes) sacrificing their privacy for future performance gains.

Google translate of their answer from finnish: "@LotusMega Service is a temporary glitch, which are working to fix as quickly as possible. Sorry for any inconvenience!"

>Oh, that article is especially trollish, but there are articles like that in both camps

Do you have any examples?

>Sometimes you need to prove `A ∨ B ⇒ C`; that's your proof goal. To do that, you prove `A ⇒ C` and `B ⇒ C`. That's all.

Yeah, I was just confused, it's just or-elimination with a different notation.

I guess "fighting" really is an appropriate word for what he's doing when he describes or-introduction as the "Act-Stupid"-rule in that composition paper.

His alternative or-composition rule looks strange to me, since given either A or B it is entirely subsumed by simple implication, but his rule still seems to need both..? Or am I missing something about his notation?

Section 6.3 also contains unsubstantiated claims about what is "popular among computer scientists" and what "many computer scientist" do or that they "denigrate the use of ordinary mathematics". I mean, this guy knows who he is talking about, why not call them out on the specifics? (He does reference one paper, and then attacks it by comparing it to a specification he worked on, which he does not reference.)

He's obviously way smarter than me, and I think I understand his general position, but it's hard to get at his arguments when he wraps them in some much hostility.

Personally I'm more interested and fascinated by the stuff going on in the Milner camp, so I'm obviously biased against him. But I do think the most fruitful approach is to have many people working in different directions and seeing what falls out, instead of trying to prove a priori that a research direction is useless.

The regulations we're talking about concerns the marking of food. You are still allowed to sell shitty vegetable oil, you're just prohibited from calling it Extra Virgin Olive Oil when you're selling it in EU. The fact that the shitty oil can be labeled whatever in the US is outside the scope and reach of the EU.

Did you check out the papers I linked to? Because they explain how this "makes sense".

Dependently typed languages allow for type-level functions (actually they erase the separation between type-level and value-level). This is why you can define a type like "Fin n" meaning a number smaller than n. "Fin n" is a function that takes one argument "n" and returns a type that limits its values to the set of (natural) numbers smaller than n.

Arguably, Agda is more often used as a proof assistant, rather than as a programming language (although I've had the pleasure of watching Ulf Norell implement a limited programming language interpreter in Agda, using non-total functions, which was quite nice.) But Idris is a serious effort to create a language that's both dependently typed and performs decently when used as a regular programming language.

If you want to see some real world examples of using dependently typed languages, I would suggest looking at the CompCert C Compiler[0]. It is a C Compiler that's been formally verified using the Coq proof assistant, which is a precursor to both Agda and Idris. Coq is as far as I know the first dependently typed language.

To be fair, programming in a dependently typed language usually requires more effort upfront, but the ability to encode properties that are usually considered runtime errors into the type system does seem like an interesting future for programming languages.

[0] http://compcert.inria.fr/compcert-C.html

(edit: shout out to the excellently named sibling commenter "curryhoward", IMHO one of the most interesting results in programming language technology and type theory research!)

Probably with a function with a type signature something like this (which is in Agda, another dependently typed language, but the idea holds):

    nGram : {l : Nat}{n : Fin l} -> Vec l Char -> n -> List (Vec n Char)

To break it up:

    "nGram" is the name of the function
    
    "{l : Nat}" means l is a natural number
    
    "{n : Fin l}" means n is a finite number smaller than l
    
    "Vec l Char" is the first argument, declared as a 
    vector of characters, with length l
    
    "n" is the second argument (previously declared as
    a finite number smaller than l)
    
    "List (Vec n Char)" is the return type, a list which consists 
    of vectors of characters where each vector is of length n

For an explanation on how and why this works you can check out these papers:

http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf

http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWo...

The first is more about programming in Agda while the second goes into how dependently typed languages relate to logic. Together they provide sufficient definitions of Nat, Fin, Vec and List to declare the nGram function.

If you're unfamiliar with ML-style syntax the above definiton probably looks weird, but can be written in a pseudo-java style like this:

   List<Vec<N,Char>> nGram<Nat L,Fin<L> N>(Vec<L,Char> input_string, N n){}

> This hasn't changed

Serious Eats has at least given conflicting advice on the topic less than a year after that article was published: http://www.seriouseats.com/2015/03/cooking-with-olive-oil-fa...

Which I think perfectly illustrates the problem.

Dropbox also have a desktop client that's written in python. Presumably with a slightly different UI layer and packaging method depending on the target OS, but with the underlying functionality shared.

I'm guessing it's this case he's referring to: http://www.theregister.co.uk/2008/12/07/brit_isps_censor_wik...

Louis CK: 'I never viewed money as being "my money" I always saw it as "The money" It's a resource. if it pools up around me then it needs to be flushed back out into the system.'

I don't think his point is that this money exists in some sort of limbo where it's not his, because however he views it, it's still his money. I think he's making a general statement about how he views money: as a resource to be used, not a collectible to be amassed.

You are, however, apparently comfortable with (indirectly) accusing Joshua Kaufman of violating a man's privacy, in a public forum without a conviction in a courtroom. Why won't you afford him the same presumption of innocence?

At least he contacted the police first, who wouldn't act on the evidence and only then did he try to garner public support for his case by showing the world the evidence he had. He even did this without accusing the man in the pictures of anything other than possessing his laptop, which is a fact arising from the evidence, even if it hasn't been considered by a court. This case wouldn't even reach a courtroom if it weren't for the fact that this website eventually got the attention of the police.

Ideally the police should have just taken the evidence and investigated the case, but instead the justice system failed. What options did this guy have, other than drawing attention to the fact that the police didn't do their job? Grabbing his pitchfork and willfully instigating a real lynch mob? Letting his computer go?

Good question.

Copyright is concerned with protecting original works, so it depends on what exactly you're referring to by "API". My interpretation is that the technical document describing an API is an original work and that the library implementing an API is an original work (provided they do not copy or modify existing works protected by copyright, then they are derivative works), but the idea the API conveys is not protected by copyright (this is what's known as the idea-expression divide[1]).

This is further complicated by the fact that we're discussing the law here so we can't assume anything to be logical or consistent. In the US, the DMCA have specific portions concerning the legality of reverse engineering for various purposes, which have implications for someone wishing to write an independent implementation of an API[2]. Maybe someone would argue that any implementation written according to the API specification is a derivative work?

I don't think there's a definitive answer to your question, since AFAIK this haven't been tested in court. In fact, in the ongoing patent/copyright dispute between Oracle and Google, Oracle claims Google violated Oracle's copyright by reproducing Java API's in Android[3].

(Disclaimer: IANAL, and I've probably misinterpreted something along the way)

[1] http://en.wikipedia.org/wiki/Idea-expression_divide

[2] http://stackoverflow.com/questions/1094103/is-copying-an-api...

[3] http://www.groklaw.net/pdf2/OraGoogle-36.pdf (p. 9)

Only the the actual implementation code (and subsequent compiled result) is under copyright, anyone is free to write an independent implementation that's not based on any of the original copyrighted code.

(There is of course the possibility of patents covering the innovations in the SNES, but that's a separate issue from copyright, and I have no idea how software patents in Japan worked around the time the SNES got released.)

>But it’s clear that in the early part of the 20th century, the original advent of the motor car was not impeded by anything like the current mélange of regulations, laws and lawsuits.

They did try in the 19th century though, at least in the UK, with the Locomotive Acts[1]. The way those laws went out of their way to protect the status quo (i.e. horse-powered transport) is an interesting parallell to today's possible transition from human-controlled to computer-controlled transport.

[1] http://en.wikipedia.org/wiki/Locomotive_Acts

That looks like a paraphrasing of Parkinson's Law[0]

[0]http://en.wikipedia.org/wiki/Parkinsons_Law

Bookmarklet: https://github.com/niyazpk/Collapsible-comments-for-Hacker-N... and Chrome extension: https://chrome.google.com/webstore/detail/hockhafcdegocajmjh...

(I've only tested the Chrome extension, but it's based on the bookmarklet so that one should work to.)