7 ms·

What is it about Haskell that makes it a hot candidate for use in cryptocurrency applications? Can someone here shed some light? Read the article but it mostly

What is it about Haskell that makes it a hot candidate for use in cryptocurrency applications? Can someone here shed some light? Read the article but it mostly seems to be a diatribe against crypto on philosophical grounds. I wish it were meatier on the technical reasons for this alleged relationship between Haskell and crypto industry.

dtseng123 6y ago
There's no actual technical reason. People fell into this as typesafe = "code must safe & secure". Its also a difficult language to understand unless you've trained under it compared to others. There's an innate obfuscation as a result.
BreakfastB0b 6y ago
There’s a deep connection between Types and Logical Proofs (Curry Howard Correspondence). Haskell has a rich type system that allows you to “prove” (i.e. typecheck) many properties of your program. This is valuable when getting right the first time is important such as smart contracts. I put prove in quotations because all type systems of Turing complete languages are unsound, but this doesn’t matter too much in practice. If you wanted to be really sure, you’d use a total language like Idris or Coq.
- bodhiandpysics1 6y ago
  That's not true... all turing complete type systems are unsound (where the type metalanguage itself is a turing complete language), but you can have a sound type system of a turing complete language, and in fact haskel itself has such a type system.
  - xkapastel 6y ago
    I think it's the possibility of nontermination that leads to unsoundness. You can construct a well-typed program that never produces a result, which means the fact that a program has a particular type does not mean you've proved a particular proposition.
  - chriswarbo 6y ago
    Haskell's type system is unsound. Here's an example, where we can prove that 1 + 1 = 1: {-# 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 The unsound proof works because our type 'Equal a b' doesn't only contain proofs that a = b (AKA 'Refl'); it also contains infinite loops, like 'falsePositive = falsePositive' (AKA "bottom"). We can use this to undermine any guarantee we try to enforce using Haskell's type system. In fact, we can make a generic version, which can be used to satisfy any type constraint: loop :: forall a. a loop = loop In theory, any time we actually try to use 'loop' our program will freeze; so we might think we're safe from any bad consequences; e.g. if we have 'launchTheMissiles :: PresidentialApproval -> IO ()' we can trick it with 'launchTheMissiles loop', but we're safe since that program contains an infinite loop, right? 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).
  - deleted 6y ago
    [deleted]
  - BreakfastB0b 6y ago
    All types in Turing complete languages are inhabited by non terminating terms (looping forever, throwing exceptions), which means all propositions are provable. For instance in Typescript, const absurd = <A>(): A => absurd() const unimplemented = <A>(): A => { throw new Error(“Unimplemented”) } const uninhabited: string & number = absurd() Intuitively you can think of it like, “Yeah sure, I can build you a term of any possible type, as soon as I get back to you.”, but then the function just ghosts you by looping forever. But it hasn’t lied. However, so long as you’re aware of these gotcha’s they don’t come up much in practice which is why viewing types as proofs is still useful. Just don’t stake your career on one.
twat 6y ago
Haskell always struck me as a language you'd want to use to feel superior to the people who code in JS and python, and crypto always struck me as a field you'd want to work in to feel superior to the people who work in industries that actually generate profits. 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?
- tsss 6y ago
  Do you even know what "verbose" means? Haskell is obviously the exact opposite of verbose. In fact some more verbosity often makes it easier to understand.
  - rjknight 6y ago
    In context, the "language" GP was referring to was the (presumably English) language in crypto currency white papers which is "needlessly convoluted and verbose". This was being contrasted with the concise language of the original Bitcoin white paper. It's not about programming languages.
    - twat 6y ago
      Yea what this guy said ^
- 1tCKV3QfIo 6y ago
  Just say you don't want to learn more than the absolute minimum when it comes to programming language theory. No one will give you shit if you are honest about it.
pyb 6y ago
This is touched upon in the text : "the Haskell community itself has simply become a tool to buy legitimacy and pump token values."
- twat 6y ago
  I was at a hackathon and this big shot legal person from NY was telling me about a hot crypto company and them using Haskell was like the first thing he told me. In fact, all he told me was they raised a bunch of money in an ICO and they use Haskell. And then he sat there waiting for me to be impressed
  - sitkack 6y ago
    Middle-out block exchange gets you 2x the fees and 1/4 the confirmation latency. Add in "and every dev gets dual monitors" and it would have been 1999.
  - analyte123 6y ago
    Every company that has the ability to do this as a recruiting tool will do it. We're using Elixir / we're using OCaml / we're using Clojure (we're using NLP / we're using ML). In every case there will be some "business" guy who understands just enough to try to impress some potential recruit. If you don't understand the domain and their actual usage of the tool or language enough to fall for this and not ask further questions, it's kind of a problem on your part.
danpalmer 6y ago
> What is it about Haskell that makes it a hot candidate for use in cryptocurrency applications? 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.
- prionassembly 6y ago
  Apparently there's "right wing" people in Haskell now. This is such a paper thin threat on unspecified persons who must know they're being targeted. 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?
  - HelloNurse 6y ago
    Are you saying that cryptoscammers are "right wing", or that threatening cryptoscammers to get rid of them is "right wing"? In what sense dealing with "unsavory varieties" can be considered a partisan issue?
  - chriswarbo 6y ago
    The influx of money is toxic because Haskell's traditional reputation (roughly: difficult to learn, but fast, smart & correct) is being co-opted to add a veneer of legitimacy to crypto scams. 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".
bodhiandpysics1 6y ago
There is a certain class of computer programs that can best be described as a really big table. Basically, an input taken from a finite set, you get an output taken from a finite set. This type of program is really easy to write in Haskel because you can prove that both the conplete input set and output set are covered using the type system. In other words you can prove that you deal with every possible case (though you can't prove that you deal with every possible case correctly!!!), and that there is no ambiguity (one input has multiple correct outputs) A good example of such a program is an insurance contract (or a derivitive contract in a bank)
- CyberDildonics 6y ago
  That's basically a DAG - directed acyclical graph. Data is transformed from inputs to outputs with no state or branching on the macro level of the transform. Lots of programs have parts that map to this very well. The cracks show when someone realizes this and thinks it is a silver bullet to build an architecture that ONLY does this. Then the parts that inevitably do need branching, state, and complex loops become a big problem. Combined with resource management (which can be thought of as mixing in branching and state) and the simplistic approach that seemed like a silver bullet turns into a nightmare once the realities of real software set in.
  - pwm 6y ago
    Hm, what's the issue with state and branching?
    - CyberDildonics 6y ago
      If you build a language that is based around doing everything with stateless data transformations but doesn't address state and branching, it will eventually be a problem, because the reality is that the vast majority of non trivial software needs to deal with plenty of state and branching, not to mention the state and branching that will go in to managing resources. 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.
heavenlyblue 6y ago
It attracts the same kind of intellectuals who like the idea of cryptocurrency. It's like a double-whammy.

dtseng123 6y ago

There's no actual technical reason. People fell into this as typesafe = "code must safe & secure". Its also a difficult language to understand unless you've trained under it compared to others. There's an innate obfuscation as a result.

BreakfastB0b 6y ago

There’s a deep connection between Types and Logical Proofs (Curry Howard Correspondence). Haskell has a rich type system that allows you to “prove” (i.e. typecheck) many properties of your program. This is valuable when getting right the first time is important such as smart contracts. I put prove in quotations because all type systems of Turing complete languages are unsound, but this doesn’t matter too much in practice. If you wanted to be really sure, you’d use a total language like Idris or Coq.

bodhiandpysics1 6y ago
That's not true... all turing complete type systems are unsound (where the type metalanguage itself is a turing complete language), but you can have a sound type system of a turing complete language, and in fact haskel itself has such a type system.
- xkapastel 6y ago
  I think it's the possibility of nontermination that leads to unsoundness. You can construct a well-typed program that never produces a result, which means the fact that a program has a particular type does not mean you've proved a particular proposition.
- chriswarbo 6y ago
  Haskell's type system is unsound. Here's an example, where we can prove that 1 + 1 = 1: {-# 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 The unsound proof works because our type 'Equal a b' doesn't only contain proofs that a = b (AKA 'Refl'); it also contains infinite loops, like 'falsePositive = falsePositive' (AKA "bottom"). We can use this to undermine any guarantee we try to enforce using Haskell's type system. In fact, we can make a generic version, which can be used to satisfy any type constraint: loop :: forall a. a loop = loop In theory, any time we actually try to use 'loop' our program will freeze; so we might think we're safe from any bad consequences; e.g. if we have 'launchTheMissiles :: PresidentialApproval -> IO ()' we can trick it with 'launchTheMissiles loop', but we're safe since that program contains an infinite loop, right? 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).
- deleted 6y ago
  [deleted]
- BreakfastB0b 6y ago
  All types in Turing complete languages are inhabited by non terminating terms (looping forever, throwing exceptions), which means all propositions are provable. For instance in Typescript, const absurd = <A>(): A => absurd() const unimplemented = <A>(): A => { throw new Error(“Unimplemented”) } const uninhabited: string & number = absurd() Intuitively you can think of it like, “Yeah sure, I can build you a term of any possible type, as soon as I get back to you.”, but then the function just ghosts you by looping forever. But it hasn’t lied. However, so long as you’re aware of these gotcha’s they don’t come up much in practice which is why viewing types as proofs is still useful. Just don’t stake your career on one.

twat 6y ago

Haskell always struck me as a language you'd want to use to feel superior to the people who code in JS and python, and crypto always struck me as a field you'd want to work in to feel superior to the people who work in industries that actually generate profits. 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?

tsss 6y ago
Do you even know what "verbose" means? Haskell is obviously the exact opposite of verbose. In fact some more verbosity often makes it easier to understand.
- rjknight 6y ago
  In context, the "language" GP was referring to was the (presumably English) language in crypto currency white papers which is "needlessly convoluted and verbose". This was being contrasted with the concise language of the original Bitcoin white paper. It's not about programming languages.
  - twat 6y ago
    Yea what this guy said ^
1tCKV3QfIo 6y ago
Just say you don't want to learn more than the absolute minimum when it comes to programming language theory. No one will give you shit if you are honest about it.

pyb 6y ago

This is touched upon in the text : "the Haskell community itself has simply become a tool to buy legitimacy and pump token values."

twat 6y ago
I was at a hackathon and this big shot legal person from NY was telling me about a hot crypto company and them using Haskell was like the first thing he told me. In fact, all he told me was they raised a bunch of money in an ICO and they use Haskell. And then he sat there waiting for me to be impressed
- sitkack 6y ago
  Middle-out block exchange gets you 2x the fees and 1/4 the confirmation latency. Add in "and every dev gets dual monitors" and it would have been 1999.
- analyte123 6y ago
  Every company that has the ability to do this as a recruiting tool will do it. We're using Elixir / we're using OCaml / we're using Clojure (we're using NLP / we're using ML). In every case there will be some "business" guy who understands just enough to try to impress some potential recruit. If you don't understand the domain and their actual usage of the tool or language enough to fall for this and not ask further questions, it's kind of a problem on your part.

danpalmer 6y ago

> What is it about Haskell that makes it a hot candidate for use in cryptocurrency applications? 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.

prionassembly 6y ago
Apparently there's "right wing" people in Haskell now. This is such a paper thin threat on unspecified persons who must know they're being targeted. 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?
- HelloNurse 6y ago
  Are you saying that cryptoscammers are "right wing", or that threatening cryptoscammers to get rid of them is "right wing"? In what sense dealing with "unsavory varieties" can be considered a partisan issue?
- chriswarbo 6y ago
  The influx of money is toxic because Haskell's traditional reputation (roughly: difficult to learn, but fast, smart & correct) is being co-opted to add a veneer of legitimacy to crypto scams. 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".

bodhiandpysics1 6y ago

There is a certain class of computer programs that can best be described as a really big table. Basically, an input taken from a finite set, you get an output taken from a finite set. This type of program is really easy to write in Haskel because you can prove that both the conplete input set and output set are covered using the type system. In other words you can prove that you deal with every possible case (though you can't prove that you deal with every possible case correctly!!!), and that there is no ambiguity (one input has multiple correct outputs) A good example of such a program is an insurance contract (or a derivitive contract in a bank)

CyberDildonics 6y ago
That's basically a DAG - directed acyclical graph. Data is transformed from inputs to outputs with no state or branching on the macro level of the transform. Lots of programs have parts that map to this very well. The cracks show when someone realizes this and thinks it is a silver bullet to build an architecture that ONLY does this. Then the parts that inevitably do need branching, state, and complex loops become a big problem. Combined with resource management (which can be thought of as mixing in branching and state) and the simplistic approach that seemed like a silver bullet turns into a nightmare once the realities of real software set in.
- pwm 6y ago
  Hm, what's the issue with state and branching?
  - CyberDildonics 6y ago
    If you build a language that is based around doing everything with stateless data transformations but doesn't address state and branching, it will eventually be a problem, because the reality is that the vast majority of non trivial software needs to deal with plenty of state and branching, not to mention the state and branching that will go in to managing resources. 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.

heavenlyblue 6y ago

It attracts the same kind of intellectuals who like the idea of cryptocurrency. It's like a double-whammy.