Is there any falsifiable evidence in this article? All I read was a big advertisement for a recuiter named Jon Marcus, with a bunch of assertions about how companies could recruit better if they only lowered their standards. Of course you can increase your yield if you accept lower quality. That's as true in manufacturing as it is in human resources.

"He’s interviewed Ivy Leaguers and dropouts; and as a result, he has helped shape countless “A teams” and every other kind of team, then watched those teams suceed or fail."

Really? I've never seen a recruiter follow up with any candidate whatsoever, and I've interviewed hundreds of candidates from the employer side. So I have serious doubts about his ability to shape or understand how a candidate can affect an organization. The feedback loop just doesn't exist - companies don't provide outside entities (recruiters) feedback about their hired employees. The legal risk alone is too high.

Case in point: "[Y]ou don’t need the whole staff to be engineering geniuses. You need a couple really bright people who know what they’re doing, and then, just don’t turn down people who can do the job."

really, I only need a couple of people who know what they're doing? What exactly are the rest of the engineers doing? They don't know what they're doing, but can follow instructions from those who do? I'd rather just not hire those people to begin with. According to Jon Marcus then, I'm part of the problem. Except, he has a real financial incentive to place marginal people, since he gets 20-25% of the first year salary. What do you think that does to his opinion of hirability?

The Daily Show

From what I've seen, a Master's degree is not much more than finishing school for people who went to unremarkable undergraduate programs.

I think the "final words" are the definition of 'obsequious'. Say something of real substance, and commit to it:

"Haskell and Scala are both very powerful and practical programming languages, but with different strengths and weaknesses. Neither language is perfect and I think there is room for improvements in both. I will definitely continue to use both of them, at least until something better shows up. Some new interesting ones on my radar are Rust, ATS and Idris."

"I think the "final words" are the definition of 'obsequious'. Say something of real substance, and commit to it:"

Because someone isn't a fanboy and isn't just stupidly commiting himself to one thing, than he's obsequious? Well, I would call this a smart person.

Types are propositions, and programs are proofs. If your program satisfies the type, then it is a proof of the proposition.

That is true, but the proposition is one that is encoded in the type. There are many derivations of certain proofs. Consider:

    map :: (a -> b) -> [a] -> [b]

And [a] is shorthand for a recursive type: \forall a . \mu l . (a * l) + ().

And the translation of types to propositions means that the sum type -- either I have () or I have a list, translates to a logical connective of "or". The product type -- I have an a and the rest of the list -- translates to "and" .

The proposition is therefore that, for all a, for all b, if a implies b, then true or (a and list of a) implies true or (b and list of b).

There are several proofs of this proposition, and some of them are useless.

The standard one:

    map f []     = []
    map f (x:xs) = f x : map f xs

Is what we want.

There's another one, though:

    map f []     = []
    map f (x:xs) = [f x]

And many others that aren't so useful as the standard one.

Anyway, this has been a long and roundabout way of saying that, while a good type system give you a lot of nice static properties about a program, you simply cannot ignore dynamic semantics and rely on the types. Well-typed programs are correct in that they will not reach a state where evaluation is undefined / get stuck ("I'm supposed to do what? These are Strings, not Ints!"), but they do not imply correctness of the program, even though they do provide a proof of a proposition!

In Haskell all types are inhabited, so every proposition has a proof. This makes Haskell a pretty useless logic.

Some of them are only inhabited by bottom, no? I cannot write down a function f :: a -> b besides:

    f :: a -> b
    f = undefined

There are a lot of other Haskell features you can use. Term-level recursion works:

  f :: a -> b
  f = f

Type-level recursion works, even without explicit term-level recursion:

  data T a b = C (T a b -> (a -> b))
  
  q :: T a b -> (T a b -> (a -> b))
  q (C f) = f

  w :: T a b -> (a -> b)
  w x = (q x) x

  f :: a -> b
  f = w (C w)

This is basically encoding Russell's paradox at the type level. You can write out f explicitly, just so that it doesn't look like you might somehow still be applying w to itself recursively:

  g :: a -> b
  g = (\x -> ((\(C f) -> f) x) x) (C (\x -> ((\(C f) -> f) x) x))

There are even ways of doing this using highly impredicative definitions involving GADTs and type families, without involving any explicit recursion at all:

http://okmij.org/ftp/Haskell/impredicativity-bites.html

The GADT example no longer seems to work, so changes to GADT type checking might have eliminated it, but the type family one still does.

It doesn't affect your objection to MaleKitten but not all types are occupied in Haskell. You are thinking of kind * By contrast,

    {-#LANGUAGE DataKinds#-}
    a :: 'Nothing
    a = a

and

    {-#LANGUAGE MagicHash#-}
    import GHC.Prim
    a :: Int#
    a = a

don't typecheck, though I cant say I understand the ins and outs of the latter.

"ps: Help get this on the frontpage of HackerNews"

Actually, I think you bear the burden of proof here by asking to get this to the front page. Asking for evidence and reasoning is hardly trolling.

I was referring to yhud previous comment on being naive. Asking questions such as yours is indeed not trolling and apologize for the confusion.

As for your question there is as far as we know little news coming from Syria and rejon who is commenting here as well is on the case to get more info.

MaleKitten, yhud said both "you are speaking about 'legal charge' and about a country like Syria at the same time ... How naive are you?" and "unjustly how?".