[ux266478]

> Metamath is based on set theory, and would therefore address some concerns one might have with the propositions-as-types philosophy used by Lean

Isn't the entire point mathematicians adopted Lean where they spurned Haskell is because of the batteries-included ZFC object language in the former? Metamath implements a set theory object language just the same, it's not based on it at all in this sense. You just changed one metalanguage for another.

[eru]

I don't think Haskell would have been useful anyway? You'd want a dependently typed language for this, not Haskell. Haskell's types can't really express anything non-trivial.

[solomonb]

Correct. There are awful tricks to write [1] dependent Haskell but even then it isn't powerful enough and has a significantly worse user experience then a proper dependently typed proof checker (as bad as the UX is on those!).

That said there are other languages such as Agda, Idris, and Rocq that would be fantastic replacements to Lean, especially if you care about staying constructive.

1. https://homepages.inf.ed.ac.uk/slindley/papers/hasochism.pdf

[ux266478]

I mentioned in another comment, but that worse user experience is also going to exist with Idris. It's not a theorem prover, you can just use it as one.

[solomonb]

Idris has pi and sigma types, dependent pattern matching, view patterns, totality checking, proof search, interactive case splitting, etc, etc.

It is orders of magnitude better then Haskell where the best you can do is hacky bullshit with singletons, GADTs, and type families.

[ux266478]

Sure, but what I'm saying is that still doesn't make it nice to use as a proof assistant. As you say, the UX isn't there, no matter how much more terse the type system is at certain things in native semantics. Idris is designed to express executable programs, it has a wildly different grain to it than Lean or any other system designed to be used as a general proof assistant from the ground up.

[solomonb]

I agree that Lean or any of the other languages I listed would be a better choice then Idris and despite how I wrote my original post I wouldn't recommend Idris to someone who explicitly wanted a theorem prover.

[ux266478]

That's not quite right, Haskell's type system is fully turing complete. Strictly speaking, it can encode anything any other program can. If we put aside language extensions, I can see a pragmatic and ergonomic limitations obviously, but that's not an expressibility problem, and I wouldn't really equate what remains practical with triviality. With language extensions, you can just kind of do whatever as shown by Liquid Haskell.

I can see the real pain point more being the fact that it's not like a typical proof assistant, and utilizing it as one is going to be unintuitive and strange.

https://hackage.haskell.org/package/type-settheory

[eru]

You are right, and the first version of my comment had exactly all this hedging (though less educated and sophisticated than your version).

When I said 'Haskell', I really meant 'vanilla Haskell a sane person might want to write'. Similar to how C++'s type system is fully Turing complete, but you shouldn't use it that way.