What's stronger than Haskell?

black_knight 3 hours ago | parent | next [-]

Dependent types is one possible direction. Not sure when a language with dependent types will arise which will be useful for making real programs.

Agda is the most mature dependently typed programming languae (having been around since the 90s – it is basically Haskell on steroids), but has a more proof-assistant flavor than an actual programming language flavor. Opus & Fable write Agda quite well, so LLMs can understand dependent types.

▲

astrange 3 hours ago | parent | prev | next [-]

Anything with ranged numeric types. Like everyone's favorite functional programming language, Ada.

	▲	ghaslt 2 hours ago \| parent \| next [-]
		This issue raises SIGFPE. Ada would raise Constraint_error, which is easier to catch than a signal, but still occurs at runtime. You need range proofs to be 100% safe, and then you can as well use the regular type because invalid values will not occur.
	▲	black_knight 3 hours ago \| parent \| prev [-]
		Or Liquid Haskell.

▲

TheGoddessInari 3 hours ago | parent | prev | next [-]

Lean 4, Idris 2.

▲

theLiminator 3 hours ago | parent | prev [-]

Perhaps coq/agda/idris/etc.