5 ms·

I'm starting to understand why HMTI, and OCaml/Haskell et. al., struggle from such obscurity despite its fanboys swearing by it. The problem is that it's a crap

I'm starting to understand why HMTI, and OCaml/Haskell et. al., struggle from such obscurity despite its fanboys swearing by it. The problem is that it's a crap technology in both easy mode and hard mode. - easy mode: beginners just want to learn how to program as quickly as possible, something like python is fantastic for that. And the side-benefit, you can do amazing stuff with it, like bypass whole of symbolic AI of 80s and 90s (including HMTI, OCaml/Haskell) and go straight to deep learning, BERT, GPT what not. - hard mode: mathematicians would love a helpful computing system that'll make them more productive mathematicians. When they attempt to explore stuff like Coq, and HoTT etc, the first thing that's thrown at their face is that they have to give up law of excluded middle, non-constructive logic and what not. I'm sorry but the tail does not wag the dog. If your theorem assistants and checkers require the mathematicians to turn their world upside down, most won't give a rat's ass about what you have to say about propositions-as-types and programs-as-proofs. There is a medium mode, or shall we say mediocre mode, whereby you fall in love with type-theory and type-based languages, you want to live in your own bubble and not be bothered by what's happening in the outside world. And that's were the users of these systems live.

nullc 6y ago
This would be an interesting statement of an opinion if the language were toned down a little bit from flame-broiled mode to medium well. You took all this time to write out your thoughts, why not put a little extra effort into massaging them in a way that will maximize their impact rather than just turning people off with flame-bait?
dependenttypes 6y ago
I do not get it. HM lets you do things like f x = fold g x without writing the types, how is that not easy mode compared to C or Java for example?
- WJW 6y ago
  It's easy mode when writing, not when reading.
  - dependenttypes 6y ago
    I disagree, you can have your IDE display the types if you so wish. Even then, would you say that python for example is hard mode?
    - WJW 6y ago
      In python, using single letter functions is not encouraged though. In general, I found that there is a tipping point above which more advanced the abstractions actually decrease the readability of the code because the ratio of implied to explicit code gets unbalanced. The verbosity of C/Golang/Java is actually a benefit here, since they remain readable even to new team members, hungover team members, new parents on 2 hours of sleep and generally anyone without a good model of all the implicit meaning behind the abstration in their head at this moment. This may or may not include "future me" scenarios where you come back to some overly clever code in 5 years and have to relearn 3 separate DSLs that were hip at the time. The IDE experience for Haskell also... leaves something to be desired atm. Hie and GHCIDE are cool projects but I regularly see even experienced Haskellers struggle installing them (and/or keeping them working after updates).
nimih 6y ago
On the subject of the tail wagging the dog, mathematicians have been fighting about non-constructive proofs and the law of excluded middle far longer than they've been writing proof assistants, and deriding a direction of active and fruitful research just because you're not personally interested in it seems rather myopic.
- ImprobableTruth 6y ago
  >mathematicians have been fighting about non-constructive proofs and the law of excluded middle far longer than they've been writing proof assistants Yes, and Brouwer lost that fight. Classical logic is an implicit assumption for professional mathematicians. LEM is simply taught as the truth in university courses. My SO who is a math phd student hadn't even heard of intuitionistic logic before. If you want working mathematicians to use theorem provers, they need LEM. But this isn't actually all that much of an issue, since you can just introduce LEM as an axiom. It breaks computationality, but it's not like proof assistants using classical logic would have this either.
  - a1369209993 6y ago
    > LEM is simply taught as the truth in university courses. So is[0] the notion that quantum systems magically undergo non-local, non-linear, non-unitary, CPT-violating, Liouville's-Theorem-violating, non-deterministic evolutions whenever a macroscopic system that happens to implement a sapient intellegence looks at something[1]. So that's not a very good yardstick for "this is not obviously false". 0: sample size of one univerity (circa 2010) for "simply taught as the truth", but I think it's recent enough and widespread enough to make a good example. See [2] if you want to investigate further. 1: aka the collapse postulate or Copenhagen interpretation 2: https://en.wikipedia.org/wiki/Copenhagen_interpretation#Acceptance_among_physicists https://en.wikipedia.org/wiki/Copenhagen_interpretation#Acce...
    - JoeCamel 6y ago
      I would argue that trying to describe our physical world and reality has only one "axiom" which is: your description has to be consistent with our observations of the world. Mathematics doesn't have this limitation so I don't think your example is valid. If you don't like LEM, fine, maybe there is something interesting in systems without LEM, but most math is done with LEM. I don't think is a matter of "right" and "wrong".
ImprobableTruth 6y ago
>that's thrown at their face is that they have to give up law of excluded middle, non-constructive logic and what not This is just outright false. You can introduce it as an Axiom. In Coq this is literally just Axiom classic : forall P:Prop, P \/ ~ P. I wouldn't make such patronizing statements without being very sure that I know what I was talking about. Also, mathematicians aren't the be-all and end-all. Theorem proving is also very relevant for CS, so it's not the end of the world if mathematicians keep using pen and paper for all eternity.
- kmill 6y ago
  Plus, it's a theorem in Lean: https://github.com/leanprover/lean/blob/master/library/init/classical.lean#L69 https://github.com/leanprover/lean/blob/master/library/init/... (Lean has a somewhat different type theory from Coq, where propositions in Prop have the property that all proofs of a property are defined to be equal. It turns out this along with functional extensionality (that two functions are equal iff their evaluations are all equal) is enough to get LEM, but only in Prop. Outside Prop there's a stronger commitment to constructibility. Still, every definition and lemma has some program backing it.)
  - ImprobableTruth 6y ago
    I wouldn't really say that it has a different type theory, just that it has proof irrelevance and functional extensionality build into the kernel as axioms. But yeah, it's a good way to show that you definitely don't have to give up LEM.
a1369209993 6y ago
> that they have to give up law of excluded middle They have to give up the law of the excluded middle because the law of the excluded middle is false. Counterexample: "This statement is false.". You can pretend it's true by trying to outlaw self-reference, but Godel proved that that doesn't actually work if your logic is useful enough to support arithmetic.
- JoeCamel 6y ago
  I don't understand what "LEM is false" means. What are your starting assumptions that lead to the "LEM is false" conclusion? You can use/assume LEM in your system or not, most mathematicans assume LEM (without even thinking about it).
- kmill 6y ago
  I'm not sure what you're talking about, unless you're saying truth is provability. (Classical logic would disagree.) The Lean proof assistant, which has a pretty strong commitment to constructability, has the law of the excluded middle just fine: https://github.com/leanprover/lean/blob/master/library/init/classical.lean#L69 https://github.com/leanprover/lean/blob/master/library/init/... The caveat is that it only exists in Prop, and it's a consequence of proof irrelevance and functional extensionality. Types outside Prop don't have it for the simple reason that there's no sensible way to construct an element of Either A (A -> Void) in general (this is quasi-Haskell notation, where Void is a type with no terms). I'm not sure there's any need to bring Godel into this....

nullc 6y ago

This would be an interesting statement of an opinion if the language were toned down a little bit from flame-broiled mode to medium well. You took all this time to write out your thoughts, why not put a little extra effort into massaging them in a way that will maximize their impact rather than just turning people off with flame-bait?

dependenttypes 6y ago

I do not get it. HM lets you do things like f x = fold g x without writing the types, how is that not easy mode compared to C or Java for example?

WJW 6y ago
It's easy mode when writing, not when reading.
- dependenttypes 6y ago
  I disagree, you can have your IDE display the types if you so wish. Even then, would you say that python for example is hard mode?
  - WJW 6y ago
    In python, using single letter functions is not encouraged though. In general, I found that there is a tipping point above which more advanced the abstractions actually decrease the readability of the code because the ratio of implied to explicit code gets unbalanced. The verbosity of C/Golang/Java is actually a benefit here, since they remain readable even to new team members, hungover team members, new parents on 2 hours of sleep and generally anyone without a good model of all the implicit meaning behind the abstration in their head at this moment. This may or may not include "future me" scenarios where you come back to some overly clever code in 5 years and have to relearn 3 separate DSLs that were hip at the time. The IDE experience for Haskell also... leaves something to be desired atm. Hie and GHCIDE are cool projects but I regularly see even experienced Haskellers struggle installing them (and/or keeping them working after updates).

nimih 6y ago

On the subject of the tail wagging the dog, mathematicians have been fighting about non-constructive proofs and the law of excluded middle far longer than they've been writing proof assistants, and deriding a direction of active and fruitful research just because you're not personally interested in it seems rather myopic.

ImprobableTruth 6y ago
>mathematicians have been fighting about non-constructive proofs and the law of excluded middle far longer than they've been writing proof assistants Yes, and Brouwer lost that fight. Classical logic is an implicit assumption for professional mathematicians. LEM is simply taught as the truth in university courses. My SO who is a math phd student hadn't even heard of intuitionistic logic before. If you want working mathematicians to use theorem provers, they need LEM. But this isn't actually all that much of an issue, since you can just introduce LEM as an axiom. It breaks computationality, but it's not like proof assistants using classical logic would have this either.
- a1369209993 6y ago
  > LEM is simply taught as the truth in university courses. So is[0] the notion that quantum systems magically undergo non-local, non-linear, non-unitary, CPT-violating, Liouville's-Theorem-violating, non-deterministic evolutions whenever a macroscopic system that happens to implement a sapient intellegence looks at something[1]. So that's not a very good yardstick for "this is not obviously false". 0: sample size of one univerity (circa 2010) for "simply taught as the truth", but I think it's recent enough and widespread enough to make a good example. See [2] if you want to investigate further. 1: aka the collapse postulate or Copenhagen interpretation 2: https://en.wikipedia.org/wiki/Copenhagen_interpretation#Acceptance_among_physicists https://en.wikipedia.org/wiki/Copenhagen_interpretation#Acce...
  - JoeCamel 6y ago
    I would argue that trying to describe our physical world and reality has only one "axiom" which is: your description has to be consistent with our observations of the world. Mathematics doesn't have this limitation so I don't think your example is valid. If you don't like LEM, fine, maybe there is something interesting in systems without LEM, but most math is done with LEM. I don't think is a matter of "right" and "wrong".

ImprobableTruth 6y ago

>that's thrown at their face is that they have to give up law of excluded middle, non-constructive logic and what not This is just outright false. You can introduce it as an Axiom. In Coq this is literally just Axiom classic : forall P:Prop, P \/ ~ P. I wouldn't make such patronizing statements without being very sure that I know what I was talking about. Also, mathematicians aren't the be-all and end-all. Theorem proving is also very relevant for CS, so it's not the end of the world if mathematicians keep using pen and paper for all eternity.

kmill 6y ago
Plus, it's a theorem in Lean: https://github.com/leanprover/lean/blob/master/library/init/classical.lean#L69 https://github.com/leanprover/lean/blob/master/library/init/... (Lean has a somewhat different type theory from Coq, where propositions in Prop have the property that all proofs of a property are defined to be equal. It turns out this along with functional extensionality (that two functions are equal iff their evaluations are all equal) is enough to get LEM, but only in Prop. Outside Prop there's a stronger commitment to constructibility. Still, every definition and lemma has some program backing it.)
- ImprobableTruth 6y ago
  I wouldn't really say that it has a different type theory, just that it has proof irrelevance and functional extensionality build into the kernel as axioms. But yeah, it's a good way to show that you definitely don't have to give up LEM.

a1369209993 6y ago

> that they have to give up law of excluded middle They have to give up the law of the excluded middle because the law of the excluded middle is false. Counterexample: "This statement is false.". You can pretend it's true by trying to outlaw self-reference, but Godel proved that that doesn't actually work if your logic is useful enough to support arithmetic.

JoeCamel 6y ago
I don't understand what "LEM is false" means. What are your starting assumptions that lead to the "LEM is false" conclusion? You can use/assume LEM in your system or not, most mathematicans assume LEM (without even thinking about it).
kmill 6y ago
I'm not sure what you're talking about, unless you're saying truth is provability. (Classical logic would disagree.) The Lean proof assistant, which has a pretty strong commitment to constructability, has the law of the excluded middle just fine: https://github.com/leanprover/lean/blob/master/library/init/classical.lean#L69 https://github.com/leanprover/lean/blob/master/library/init/... The caveat is that it only exists in Prop, and it's a consequence of proof irrelevance and functional extensionality. Types outside Prop don't have it for the simple reason that there's no sensible way to construct an element of Either A (A -> Void) in general (this is quasi-Haskell notation, where Void is a type with no terms). I'm not sure there's any need to bring Godel into this....