The community opinion is that Haskell is good for building robust and correctly behaving applications. There's some evidence that very strong type systems can help with this.
Financial software is an area where people typically want deep correctness guarantees, another good example area being cryptography.
Between these I think it's probably a good thing that crypto-currency applications and applications like exchanges are being built with "safe" technology like Haskell, rather than technologies that provide much less safety (many Ethereum hacks have boiled down to Solidity contracts being relatively loosely typed).
This is however not an opinion on what crypto is doing to the Haskell ecosystem. I don't know about that.
Seriously, I don't think the readership of HN is in any disagreement about how new cryptocurrencies are "short long con" jobs, but the author teases that the influx of this money is toxic to the Haskell community because... right wing people?
I also wouldn't say the problem is to do with "right wing people". Nobody's born with a political affiliation: we learn and digest information and experience all through our lives, swinging towards and away from different values at different times. This can especially depend on our social circles, our information-bubbles, what benefits us personally, etc.
The crypto-bubble tends to discourage regulation, accountability, etc. which makes it attractive to right-wing politics, whether as a libertarian free-for-all; or money-laundering for the gentry; or whatever. When this sector has an outsized influence on a particular community, the political gradient will be tilted accordingly, and bias people's random walks to the right.
Haskell may be great at solving the technical problems with crypto, but that doesn't solve its ethical or philosophical problems. Yet, as the old saying goes, "It is difficult to get a man to understand something, when his salary depends on his not understanding it".
{-# LANGUAGE GADTs, TypeFamilies #-}
-- Peano arithmetic: these types represent '0' and '1+n'
data Zero
data Succ n
-- We can define 1 as '1+0', 2 as '1+1', and so on
type One = Succ Zero
type Two = Succ One
-- A closed type family is a function at the type level.
-- This function implements addition of the above Peano numbers.
type family Add x y where
Add Zero y = y
Add (Succ x) y = Succ (Add x y)
-- 'Equal a b' is a proof that types 'a' and 'b' are the same.
-- It works by forcing the type variable 'x' in 'Refl' to unify with both.
data Equal a b where
Refl :: Equal x x
-- The type checker will accept this proof that 1 + 1 = 2, giving:
-- >[1 of 1] Compiling Main
-- Ok, one module loaded.
truePositive :: Equal (Add One One) Two
truePositive = Refl
-- The type checker will reject this proof that 1 + 1 = 1, giving:
-- >[1 of 1] Compiling Main
-- x.hs:24:16: error:
-- • Couldn't match type ‘Zero’ with ‘Succ Zero’
-- Expected type: Equal (Add One One) One
-- Actual type: Equal One One
-- • In the expression: Refl
-- In an equation for ‘trueNegative’: trueNegative = Refl
-- |
-- 24 | trueNegative = Refl
-- |
--trueNegative :: Equal (Add One One) One
--trueNegative = Refl
-- However, the type checker will accept this (unsound) proof
-- that 1 + 1 = 1, giving:
-- >[1 of 1] Compiling Main ( x.hs, interpreted )
-- Ok, one module loaded.
falsePositive :: Equal (Add One One) One
falsePositive = falsePositive
loop :: forall a. a
loop = loop
Wrong! Haskell is lazy, so it won't bother evaluating arguments which aren't needed. Even if we try forcing the value, we can't be sure that the compiler won't optimise it away! In practice this means that we can't rely on the mere existence of well-typed values as proof of their types; we can be sure that our data dependencies exist (i.e. those values which are forced as part of our computation, which can't be optimised away), but we still won't know that beforehand (i.e. the program may crash or freeze at any point before a particular expression, due to the presence of "bottom" somewhere).
We know Haskell's type system includes bottom as an inhabitant of every type which enables us to shrug and hand-wave away proofs of termination. As long as one understands that consequence doesn't it pass Milner's definition?
I'm happy writing proofs in Lean or Agda but having to avoid or prove termination would be a pain in the rear end for most large programs. And in practice I still think of Haskell's type system as sound. I always thought of "unsound" as programs with terms that are logically inconsistent with respect to the theorems proposed by the types, eg: early version of TypeScript or Java. Put another way, that you could write a proposition in they type system that wasn't satisfied by the program (proof).
It depends on the context, but it's certainly in common use (e.g. see https://stackoverflow.com/questions/21437015/soundness-and-c... although I switched 'positive' and 'negative' in my example: e.g. I treat 'true positive' as 'correct program was accepted', that link treats 'true positive' as 'error message was justified')
> As long as one understands that consequence doesn't it pass Milner's definition?
Milner's definition is usually summarised as "well-typed programs have well-defined behaviour". Haskell does fit this description, although certain optimisations may be unsound (e.g. library-supplied rewrite rules).
To me, the key deficiency is that Haskell can't ignore 'absurd' branches. For example, let's say we have a function like this:
foo :: a -> b -> LessThan a b -> Foo
foo Zero (Succ y) _ = bar y
foo (Succ x) (Succ (Succ y)) _ = baz x y
In Haskell we can't do this: the type of one argument can't rule-out values of another. Hence we must define those branches (or else leave the implicit "unmatched pattern" error, which is a "bottom"), and we need them to return values of type 'Foo' (which may be impossible to construct, unless we return "bottom"). This satisfies Milner's definition, but also goes too far: we're specifying well-defined behaviour for programs which aren't well-typed! In practice, this leads to redundant branches like 'Nothing -> error "Shouldn't happen"', which (a) introduce potential crashes and (b) are so close to being statically avoided!
> having to avoid or prove termination would be a pain in the rear end for most large programs
It can be. If we're being lazy, we can just wrap things in a 'Delay'/'Partial' type (described a little in the above "nat-like types" link, and also at https://news.ycombinator.com/item?id=17472926) or run proofs in Coq's Mtac language ( https://plv.mpi-sws.org/mtac )
> And in practice I still think of Haskell's type system as sound.
Me too. This tends to be called "fast and loose reasoning" https://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loo...
For instance in Typescript,
const absurd = <A>(): A => absurd()
const unimplemented = <A>(): A => { throw new Error(“Unimplemented”) }
const uninhabited: string & number = absurd()
"the Haskell community itself has simply become a tool to buy legitimacy and pump token values."
Add in "and every dev gets dual monitors" and it would have been 1999.
It's like a double-whammy.
There are a lot of domain specific tools that are used for specific tasks where the main software is taking care of architecture, high level decisions and resources. Shaders are one example of this. Trying to write non trivial software like this is problematic because the structure you are using is so disconnected from what the software needs to do.
I'm assuming you are referring to Haskell? It's a general purpose programming language so of course it handles state, branching, etc...
data Tree a = Empty | Leaf a | Node a [Tree a]
deriving stock (Show, Functor, Foldable, Traversable)
label :: Tree a -> Tree (a, Int)
label t = evalState (traverse f t) 0 where
f t' = state (\c -> ((t', c), c + 1))
This looks like it is lazily evaluating parts of a tree, which means that you aren't controlling that state, you are hoping that everything works out when you query it with regards to resources, caching, memory layout, memory freeing, etc.
In a non-trivial program that either will need to optimize memory and cpu usage to scale or be careful about how things are structured to maintain interactivity, something like this is likely to be a big problem if that tree gets big.
Also, another possible reason is that many crypto people tend to confuse complexity with ingenuity. While the bitcoin whitepaper tries to make a complex topic as simple as possible, a great many crypto companies and people purposely use language that is needlessly convoluted and verbose.
Perhaps they're doing it on purpose to seem smarter?