Hindley-Milner Type Inference (2012)
steshaw.org
steshaw.org
I could not understand why most static language required writing so many types that were easy to deduce and why people where saying that not having to write types made dynamic language better.
I can count on the finger of my hands the number of times when I needed to write explicit types in Ocaml (my single use case for explicit types in Ocaml was data deserialization).
Plus, the compiler is fast.
I'd be interested if anyone found/ran any benchmarks, though I thinks its pretty hard to write a fair compile time benchmark. I did a quick search and came across this post comparing solving the same problem with haskell/ocaml/go, which just kind of off hand mentions the compile times. OCaml versions range from 0.3-0.8s and Go was reported as ~1s.
1. C++ templates don't require you to treat the type variables as opaque; depending on what the body of a template does with its type parameters it may or may not type check depending on how the variable is instantiated. By contrast, in OCaml (and most languages) generic functions cannot assume anything about their type parameter. This means that the compiler can type check the body of the generic function once and be done, rather than having to essentially check it at every call site.
2. Aside from type checking, C++ templates generate separate code for each instantiation of the type parameters. This (generally) results in faster code as it is specialized to the type in question, but it means more code is generated, which of course takes time (and it can also bloat the executables). This is probably a bigger deal than the type checking part. By contrast, OCaml only generates one copy of the code for a function, which simply doesn't care about the types of its arguments. This is also a common implementation strategy; Java does something similar.
Note that Rust also suffers from (2), but not (1).
See https://blog.janestreet.com/why-gadts-matter-for-performance... and https://blog.janestreet.com/more-expressive-gadt-encodings-v... for why you'd sometimes want the behaviour in 2.
(I do agree, that that behaviour is a bad default.)
let a = ...
in let b = ...
in let c = ...
in let d = ...They typically mix up parametric polymorphism and ad-hoc polymorphism.
I blame C++'s templates for the confusion. (And Go people's common refusal to look much further, and especially not into academia..)
I don't think that's a fair statement, given Phil Wadler's formal work on generics in Go - "Featherweight Go" (https://arxiv.org/abs/2005.11710) - which is acknowledged here: https://blog.golang.org/generics-next-step
It's good to see that they are taking the likes of Phil Wadler serious. (Perhaps his beard helps?)
> We’d like to thank Philip Wadler and his collaborators for thinking formally about generics in Go and helping us clarify the theoretical aspects of the design.
In the older post at https://blog.golang.org/why-generics you still see them pretty much mix up parametric polymorphism and ad-hoc polymorphism.
Thanks for the link to the paper!
[1] https://github.com/ocaml/opam-repository/pull/16753
[2] https://discuss.ocaml.org/t/ocaml-4-11-first-beta-release/60...
[3] https://discuss.ocaml.org/t/ann-bap-2-1-0-release/5906/9
x = function() {
if (rand() > 0.5) {
return "abc"
} else {
return 2.01
}
}
wtf = A of string | B of float
And then you'd return A("abc") or B(2.01) and your function would be () -> wtf
I think the point you're making is that Standard ML has certain restrictions in its type system that are necessary to make type inference possible: there are no union types, no subtypes (more recent work has found a way to make subtyping compatible with full H-M), polymorphism has to be introduced explicitly with `let`, and there are no higher-kinded types. And in some cases you'd argue those restrictions might incur more code overhead compared to a language that loosens those restrictions at the cost of less reliable type inference (e.g. Scala).
That's sort-of-but-not-really true: in my experience union types and subtypes are always bad ideas and there are better alternatives for any use case where you would use them. You never actually want "String | Int", you want a type with meaningful semantics (like `Result<String, Int>`).
https://www.cs.cornell.edu/courses/cs3110/2011sp/Lectures/le...
So in the original example, you can't unify "ssdf" and the int 33, but in the re-written version B("sfd") and A(33) have the same type and can be unified.
A good discussion of this can be found in https://dev.realworldocaml.org/variants.html#scrollNav-4
randomReturner n =
if n < 0.5 then
123
else
"abc"
The 2nd branch of this `if` does not match all the previous branches:
22| if n < 0.5 then
23| 123
24| else
25| "abc"
^^^^^
The 2nd branch is a string of type:
String
But all the previous branches result in:
number
Hint: All branches in an `if` must produce the same type of values. This way, no
matter which branch we take, the result is always a consistent shape. Read
<https://elm-lang.org/0.19.1/custom-types> to learn how to “mix” types.
Hint: Try using String.toInt to convert it to an integer?
You would have to either:
- test for the type of that value in order to handle it properly,
- rely of the implicit cast rules of JS, which wouldn't be very useful here I suppose
As it has been said by others, in Ocaml (as well as in many other strongly typed languages) you can use a sum type to solve that problem.
Edit: In some languages, there is also the concept of "intersection types" which, if I understand correctly, let one also handle that sort of situation. The corresponding Wikipedia entry [1] gives a list of languages supporting that concept, and provides examples.
With "duck typing", you need to have an extra test for types which your code is not supposed to work with, whereas with sum types, the type checker will help you verify that it cannot happen.
That being said, there are situations which a strong type system will not be able to model.
Anyway, at the end of the day, what matters is that you (and your coworkers) feel comfortable with your code. I know by experience that it's not always the case.
To expand on another commenters example, suppose you have a sum type that models successful computation with a return value or a failure with an error message.
If you have tags / constructors, that's all easy. But if you just use naked unions, you can not write code that deals with error messages (or strings in general) in the success case.
- if true then "abc" else 2.01;
stdIn:1.2-1.30 Error: types of if branches do not agree [tycon mismatch]
then branch: string
else branch: real
in expression:
if true then "abc" else 2.01
- datatype string_or_real = r of real | s of string;
- if true then s "abc" else r 2.01;
val it = s "abc" : string_or_realHere's an example where the feature can save you:
```
let x = () => {
if (Math.random() > 0.5) {
return "abc"
} else {
return 4
}
// ERROR: This condition will always return 'false' since the types '"abc" | 4' and '"sdf"' have no overlap.
if (x() === "sdf") {
do_work()
```
import System.Random
x = do y <- randomIO :: IO Float -- note: this is before there are instances of randomIO for IO Int and other types
if y > 0.5 then
return (Left "abc")
else
return (Right 2.01)But otherwise you're right... they're almost never actually needed unless there's an actual ambiguity (e.g. what kind of collection should .collect() produce?)
It's pretty great. I can confidently do a whole pile of reckless-looking stuff and be reasonably confident that I've done what I intended to do once the compiler is happy.
They are inferred, and that's the point of their ergonomics, but when they are inferred incorrectly, it becomes pretty confusing and sometimes cryptic.
Do you genuinely rely on whole-program type inference? Writing fewer than ten explicit types in your whole career writing OCaml really surprises me. For example even the OCaml standard library is not written this way.
I find in practice most people explicitly type their top-level functions as if you don't this it can cause type errors at the point of use to 'poison' the function types and cause very confusing errors far away in the program. Do you not see this when you program without any explicit types?
We can see this in other projects for example Crystal which had to back-track on their goal of whole program inference, because it just doesn't really seem tractable in practice.
It feels like people get distracted by H-M inference and forget that there's a pretty nice high level language in SML or OCaml anyway (although I'd rather have modular implicits).
Am I wrong in thinking implementation would be much simpler without type inference?
On the other hand, non-local inference can make things more complicated in some situations, depending on how hard you try. For instance, Rust gives up if you don't know the type of a variable and you try to accesses a member of it, where I once wrote a more complicated iterative solver that would see if it could infer the type of the variable from later context and return to the member access later. For example, consider the following Rust code where the compiler could figure out the types with some additional complexity but doesn't bother:
fn main() {
let a = (1..10).collect();
println!("{:?}", a.len());
let b: Vec<i32> = a;
}
error[E0282]: type annotations neededIn fact they're so similar that they can be combined to give 'bidirectional typing'. This is mostly useful for systems that are more expressive than Hindley Milner. For example, dependently-typed languages like Agda and Idris require type annotations for top-level definitions (local definitions can sometimes be inferred). Bidirectional typing is a neater approach to such hit-or-miss inference approaches, and also allows values to be inferred (your function-overloading example is a case of value inference: using the types to figure out which particular function to call).
My guess is that Rust's designers would reply that their compiler is slow enough without the complication you describe.
Just the opposite: type inference forces the type systems to remain simpler. Without type inference you could make them more complicated.
var a = 1;
slightly harder would be typing union / intersection types - e.g. this:
var a = some_test() ? "foo" : new Bar();
Now, imagine knowing nothing about what can be stored in the variable, and only seeing how it's used - this is the case for function parameters.
(x) -> x + 1;
let x = "foo" |> bar |> baz 5
Basically, there's two complications with type inference. One is type variables that you need to then "solve" - in my last example above, the type of parameter `x` would start as a type parameter α (usually denoted by Greek letters in type systems literature), then it would be "unified" with `int` when used "like" an int (i.e. passed to a function `+ : (int, int) -> int`).
This is what happens in a language with a "simple" type system like OCaml, with no subtyping. (OCaml is slightly more complicated, but still all equations that it needs to solve only involve equality (I think)). If your type system features subtyping, things get a bit more complidated.
(x) -> new List(x + 1, concat("test", x))
The other big issue type inference deals with, is generalization. If, at the end of inferring an expression's type, there are no equations involving a type variable (a bit of a simplification, but let's go with it), then it can be "generalized" - turned into polymorphic type.
(x) -> new List(x)
In your example, figuring the type of `x` is trivial compared to above - just take the return type of `baz`.
(1) Hack until I've got something stable. Note: at the start of coding I typically don't quite know what the right abstractions are, so a lot of code (and associated types) are in constant flux.
(2) Once program is stable, wrap it in a module, let the compiler work out all types and put them in as module interface.
That gives me the best of all possible worlds: type annotations at abstraction boundaries but you don't have to type them out. Writing out explicit types inhibits fast change. I wish the languages I'm using at the moment (Scala, Rust, C++) allowed a flow like that. Alas, full type inference stops being possible with more expressive typing systems.
Right - that's not global type inference. It's intra-module type-inference.
Aside, when I decide to change where I put module boundaries, full program inference helps too: I just throw away the old module definitions, draw different boundaries and re-run inference.
Because a program's types can serve as part of its documentation.
So many times I will accidentally return 42 or Result<Result<42>> when I mean to return Result<42>. With annotations, my error is instantly obvious. Otherwise I accidentally have a function that returns Result<Result<number>> and it may lead to a very weird error message when I use `foo().map(_ + 100)` somewhere else.
That's letting the computer doing more work, not less of it. Relying too much on inference can bow back into the human doing more of the work to figure out what the types actually are in a given spot.
The computer can only tell you what types your code _has_ (from inference), but not what type it _should_ have based on your intentions. Type inference can only complain when your code contradicts with itself (on a type level), but can't tell you when it contradicts with your intentions.
If you don't write out your intentions, you'd have to hover over everything to see if the inferred types differ from your expectations.
IDE hover types and collapsible type annotations (and alternatively also collapsible implementation) are still useful as a way to declutter your UI when reading code.
I think their point is that they there were vanishingly few times where they were required to write explicit type annotations. As they say, mostly when dealing with data serialization. That doesn't say whether they wrote more, however.
0: There are plenty of places where not supplying a type annotation is more trouble than just writing it. Eg (Haskell since I'm not familiar with OCaml offhand):
data Foo = FooBar Int String
| FooBaz [Int]
data Foo a b c = FooBar a b | FooBaz c
or
data Foo a b = FooBar a b | FooBaz [a]
But I agree that writing explicit type annotations is overall better practice.
quux :: a -> a
quux x = x
# quux takes any type genericly
frob y = y () ++ [()]
# frob takes some specific type, but we don't need to specify which (spoiler alert: it's () -> [()])
If you wanted to, you could use
Either (Int, String) [Int]
Not in Haskell as far as I know, but (assuming MonomorphismRestriction) there's no technical reason why
data Qwe = Q a
qwe_eps :: Qwe
qwe_eps = Q ""
It does make it easy. OCaml has a full matrix of types:
- Nominal product types (records)
- Nominal sum types (variants)
- Structural product types (objects)
- Structural sum types (polymorphic variants)
You could actually always use structural types and never have to actually define types. But OCaml people actually really like the nominal types because their typing rules are stricter and easier for people to understand. But the structural types can come in really handy, e.g. they give you a very convenient way to encode data between libraries that don't need to know about each other. E.g. there is an effort to add JSON-structured output to the OCaml compiler itself. This is using a polymorphic variant type to represent the JSON data type, to avoid having a dependency on any particular JSON library, but still being compatible with popular OCaml JSON libraries ( https://ocaml-community.github.io/yojson/yojson/Yojson/index... ).
In eg Haskell, you often write the types first, even though in principle you seldom would have to write the types at all.
I wrote up the thoughts in a post [1] that seemed to get extreme reactions from both camps [2].
[1] Type inference has usability problems. http://web.eecs.utk.edu/~azh/blog/typeinference.html
[2] HN discussion. https://news.ycombinator.com/item?id=20296123
In practice, many people use type inference when exploring and writing code; but then add explicit annotations for readability and documentation. You could even do the last step automatically.
[1] Recently have been seeing a lot more use in BuckleScript because of the JS object representation
[1] https://discuss.ocaml.org/t/function-argument-polymorphism/3...
[2] https://www.cl.cam.ac.uk/~sd601/papers/mlsub-preprint.pdf
> Their real purpose is to support subsets and supersets, which are useful all over the place.
And indeed they are super useful, e.g. I am using them to implement functions that deal with web responses: some can deal with only HTTP responses, some with only WebSocket responses, and some with either. All completely type-safe and extensible.
In Scala, a lot of libraries end up with deduction-only types—ie, types that can only be deduced, because actually typing out the type signature is very long, complicated, and filled with generics-upon-generics. I don’t find that to be a pleasant outcome—if I can’t fill in the type signature myself, trying to understand what the code is going to do ends up that much more complicated. Yet that’s not an uncommon situation.
data Address(line1: String, line2: String, postcode: String)
data User(name: String, address: Address, phoneNumber: String)
// Argument 1
{
"name": "Bob",
"address": {
"line1": "123 Fake Street",
"line2": "Beverly Hills",
"postcode": "90210"
},
"phoneNumber": "555-555-5555"
}
// Argument 2
{
"address": {
"line1": "377 Fake Street"
},
"phoneNumber": "555-555-4444"
}
// Result
{
"name": "Bob",
"address": {
"line1": "377 Fake Street",
"line2": "Beverly Hills",
"postcode": "90210"
},
"phoneNumber": "555-555-4444"
}
Scala is one of about 3 languages where you can actually write this in a nice way and it will be correctly typed. But the type you get will be:
(User, Field[Label['name], Option[String]] :: Field[Label['address], Option[Field[Label['line1], Option[String]] :: Field[Label['line2], Option[String]] :: Field[Label['postcode], Option[String]] :: HNil]] :: Field[Label['phoneNumber], Option[String]] :: HNil) => User
Now with first-class record support in the compiler you could improve this a little bit, but fundamentally there's not really any better way to write that type. Maybe if the language had first-class support for dependent types like Idris you could write ti as `(User, UpdateTo(User)) => User` or something, but the reader would still need a way to find out what `UpdateTo(User)` was concretely. So what do you do?
You do get subtyping in Ocaml with modules and "module types", but in that case you are explicitly spelling out the module types. They're not inferred.
http://stedolan.net/research/mlsub.pdf
So this can be done, though afaik there's still some theory work to be done to combine it with some of the more advanced features in modern FP languages (e.g. higher rank types)
Data deserialization is where types are most useful
When I first came across it in the gosu code base (https://gosu-lang.github.io) I said:
"Wait. That's all you do? You just take the type from the right hand side and then put it on the left hand side?"
"Yep."
"That's type inference?"
"Yep."
It called into question many aspects of my computer science education.
A pure HM type-system is pretty restrictive, so most ML family languages don't have global type inference anyway.
I recently implemented the bidirectional system in Rust from the paper you linked, it was fun (and a challenge!)
That's what they mean by local variable inference
Even in Haskell where global type inference is supported, people end up putting type signatures on all top-level declarations because doing otherwise makes code less readable and makes type error messages way too confusing. Global type inference means a single type error in a single function can be propagated by the compiler to arbitrarily faraway at the call site, or even several layers deep in a call site. Solving such errors resulting from global type inference simply isn't worth the time.
Herb Sutter's Almost Always Auto advice was not good, in my opinion. I still find I actually need to find out the actual type so when I use it it's only typically when the RHS of the assigment mentions the type, static_cast, make_unqiue etc.
I find it saves on typing but not so much for readability. There are different rules if you're writing an STL algorithm versus a final concrete program.
a = b
a : Some -> Type -> MoreType
a = f b
But the real reason is: errors. It's so much more easier to understand errors when types are explicit.
The possibility of a diverging type-level function would require the type inference algorithm to solve the halting problem.
(As I understand it at least, been a while since I got into the details)
That's not optional typing. It's just a standardized magic comment (which the reference implementation ignores). It's far from useless, but it's not adding typing to the language.
>In particular, Typed Racket’s run-time system remains largely untyped. As a result, even the completely typed configurations of our benchmarks usually import constants, functions, and classes from an untyped module in the run-time system. When these values cross this boundary at run-time, the contract system performs checks, and that imposes additional costs.
But I haven't read the whole thing. It doesn't appear to be very related - it seems to be about gradual typing in a language that does run-time checks (with ways to disable them for performance purposes).
Typed python has no additional checks than untyped. So it's still untyped. You wouldn't claim my "// int" comments add optional typing to JavaScript, would you?
---
edit: here, take it from the source instead: https://docs.python.org/3/library/typing.html Note the title is "support for type hints" and this prominent note is right at the top:
>Note: The Python runtime does not enforce function and variable type annotations. They can be used by third party tools such as type checkers, IDEs, linters, etc.
For Python itself though: if you have a syntactic element which does not change behavior in literally any way, whether present or absent and regardless of what it contains: sounds like a comment to me.
When I used to write haskell, I'd very often write a function, iterate on it until it did what I want, then infer the type of the function and insert that into the program. Now, I was relatively new to haskell, so was probably less comfortable writing types than reading them (so I assume it was nicer to have the compiler do that for me, eyeball it to check it's what I meant to do, and put it in).
I'm wondering if someone more familiar would think "alright, what type do I want my function to be", fill that in, and then write the type out?
I definitely agree that a program is more readable with types, which is why I always filled them in (I just did it afterwards!)
Usually, the functions with more imperative flavour get their implementation first, and the more functionally flavoured bits get their type first. But that's not always the case.
Sometimes I even write the QuickCheck properties first.
In agda you usually have 2 goals creating a function
* Proving a property of some other object. In this case you have to write the type first since type is the theorem you want to prove, and implementation is the proof.
* Implement a transformation. In this case, as you described you might get away first writing the impl, and then the type, but I personally never even attempt to do that since writing out the type gives me a lot to think about the implementation of the transformation. Once types are explicit, implementation usually ends up being a lot more obvious.
In Haskell, OCaml and eg Rust, the compiler can infer the type of a new variable depending on how you are using it later.
let map = HashMap::new(); // <K,V> unknown
map.insert("hello", 1);If you've done something a million times before and are familiar with how it works, you can leave off all the type hints, and it'll figure them out for you and stay out of your way so that you can work more quickly. If you make a mistake somewhere, the compiler will still tell you.
If you're doing something new, or don't quite understand something, you're free to add type hints wherever you need them to gain clarity. You can even do stuff like:
let var: () = ...;
Once you're done, you can tidy up if you think it makes your code more readable. You can still leave top level hints to be kind to your coworkers or future you.
I think the ability to dynamically shift between "cautious exploratory mode" and "reckless I-know-what-I'm-doing mode" at the drop of a hat is why you hear a lot of anecdotes about people using languages like OCaml or Rust as if they were scripting languages.
let foo = vec![1, 2, 3];
let foo: Vec<i32> = vec![1, 2, 3];
>Finally, dynamically typed programming in Haskell made easy! Tired of making data types in your Haskell programs just to read and manipulate basic JSON/CSV files? Tired of writing imports? Use dynamic, dynamically typed programming for Haskell! [1]
If using an HM type system is really as easy and as fluid as you suggest, what purpose would be served by a type such as Haskell's Dynamic?
Nor is Dynamic a panacea: to use it requires a lot of extra typing (er, extra keypresses) IIRC, and
>A Dynamic may only represent a monomorphic value; an attempt to create a value of type Dynamic from a polymorphically-typed expression will result in an ambiguity error (see toDyn). [2]
1: https://hackage.haskell.org/package/dynamic
2: https://hackage.haskell.org/package/base-4.14.0.0/docs/Data-...
https://hackage.haskell.org/package/base-4.14.0.0/docs/src/D...
Also notice that Dynamic is in the Haskell Package Repository's "base" package, described as containing "Basic libraries", not part of an ancillary area for user-contributed libraries:
https://hackage.haskell.org/package/base-4.14.0.0
There exist type systems of which great grandparent is an accurate description (the most well-known of which is probably that used by Typescript) but the type system of, e.g., Haskell, Ocaml or Rust is not it.
(Now I am getting curious what specific programming language's type system great grandparent had in mind.)
https://hackage.haskell.org/package/dynamic
Which is an entirely different package, and the relevant types are entirely different. Only the name is the same. The `dynamic` package does indeed appear to be an april fools joke.
The Dynamic type in base is about runtime reflection, which is occasionally useful but not something that comes up often and not really about rapid prototyping.
>The Dynamic type in base is about runtime reflection, which is occasionally useful but not something that comes up often
It is not something that comes up often, but since I am used to languages like Javascript or Scheme, when it does come up, figuring out how to do it in Haskell, e.g., satisfying the monomorphic restriction, has occasionally diverted my focus away from the problem to be solved for hours while I learn more about Haskell's type system.
But yeah, what I just wrote is in no way inconsistent with the comment I initially replied to, namely,
https://news.ycombinator.com/item?id=23795687
so I am going to admit that my comments in this thread have not exactly improved the level of discourse.
Parser combinators, monads, monad transformers, curry-howard. Think for 15 minutes, write 5 lines of code, repeat. What I remember is that was code was really elegant but brain hurt so much.
I really wish I could do more FP, but the languages and libraries I use for my day-job aren’t as-accommodating (mostly C#) - while C# has some FP features, it’s really held-back by the CLR’s type-system - so until that fundamental plumbing gets done we’ll never see features like type-classes, true immutable types, algebraic-types, and so on. Without those features we’ll have to keep on writing more code than is necessary.
<digress>Heck, it’s bad enough that IDictionary doesn’t implement IReadOnlyDictionary - or that none of the IReadOnly* types make any guarantees about immutability, which means having to review documentation or disassembly in ILSpy. And the famed non-nullable-reference-types in C# 8.0 is actually all just syntactic sugar for yet more attributes rather than true code-contracts, a built-in Option type, or extending the CLR’s type-system to understand nullability. Grumble.</digress>
IIRC you just described some features of F#, excepting type classes. Or at least F# gets you closer to the goal.
Maybe the ever elusive F* has that stuff?
(I mean, "overly complicated" is bad news no matter what the specifics of what we're talking about, but how does it cause pain when it's specifically in the types?)
This is a shame, because sum types (e.g. Shape := Circle U Square U Triangle) are actually pretty useful, and languages such as Java ended up implementing them via class or interface inheritance. Languages often also required type coercion to deal with things like 0.2 + 5, otherwise + could have had a type signature like: float U int -> float U int -> float U int.
On practice nobody cares. It being undecidable just means you need an extra check at your compiler to verify the types are converging, and a new error for the problematic case.
I'm interested in what types I need to solve my business problem. The rest of it, I don't care. The reason I care about the types I need for my business problem is that I don't want my code doing something that it shouldn't: DDD-style coding allows me to code in such a way that it's impossible for the program to exist in a state that's invalid. That's a great time-saver. Other than that, polymorphic coding FTW.
http://steshaw.org/hm/hindley-milner.pdf I found this 30 page PDF document very helpful in understanding the Algorithm.
- 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.
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?
Even then, would you say that python for example is hard mode?
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).
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.
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#Acce...
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.
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.
(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.)
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.
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/...
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....