3 ms·

I think AI will push programming languages in the direction of stronger hindly milner type type checking. Haskell is brutally hard to learn but with enough of a

I think AI will push programming languages in the direction of stronger hindly milner type type checking. Haskell is brutally hard to learn but with enough of a data set to learn from, its the perfect target language for a coding agent. its high level, can be formally verified using well known algos and a language server could easily be connected with the ai agent via some mcp interface.

seanmcdirmid 1y ago
We might see wider adoption of dependently typed languages like Agda. But limited corpus might become the limiting factor, I’m not sure how knowledge transfers as the languages get more different.
- ipnon 1y ago
  It's getting cheaper and cheaper to generate corpora by the day, and Agda has the advantage of being verifiable like Lean. So you can simulate large amounts of programs and feed these back into the model. I think this is a major reason why we're seeing remarkable improvements in formal sciences like the recent IMO golds, and yet LLMs are still struggling to generate aesthetically pleasing and consistent CSS. Imagine a high schooler who can win an IMO gold medal but can't center a div!
  - andrewflnr 1y ago
    It seems like "generating" a corpus in that situation is more like a search process guided by prompts and more critically the type checker, rather than a straight generation process right? You need some base reality or you'll still just have garbage in, garbage out.
tsimionescu 1y ago
> can be formally verified using well known algos Is there any large formally verified project written in Haskell? The most well known ones are C (seL4 microkernel) and Coq+OCaml (CompCert verified C compiler).
- aetherspawn 1y ago
  Well, Haskell has GADTs, new type wrappers and type interfaces which can be (and are often) used to implement formal verification using meta programming, so I get the point he was making. You pretty much don’t need to plug another language into Haskell to be satisfied about certain conditions if the types are designed correctly.
  - tsimionescu 1y ago
    Those can all encode only very simplistic semantics of the code. You need either a model checker or dependent types to actually verify any kind of interesting semantics (such as "this sort function returns the number in a sorted order", or "this monad obeys the monad laws"). GADTs, newtypes and type interfaces are not significantly more powerful than what you'd get in, say, a Java program in terms of encoding semantics into your types. Now, I believe GHC also has support for dependent types, but the question stands: are there any major Haskell projects that actually use all of these features to formally verify their semantics? Is any part of the Haskell standard library formally verified, for example? And yes, I do understand that type checking is a kind of formal verification, so in some sense even a C program is "formally verified", since the compiler ensures that you can't assign a float to an int. But I'm specifically asking about formal verification of higher level semantics - sorting, monad laws, proving some tree is balanced, etc.
- gizmo686 1y ago
  seL4 has a Haskell implementation. It only runs under a simulator (as opposed to on real hardware). Their main proof strategy is to prove the Haskell version correct; then prove the C version matches the Haskell version.
  - tsimionescu 1y ago
    I admit that I was not aware of their use of Haskell, so thanks for bringing this up! It motivated me to go and actually read (parts of) their paper [0]. > Their main proof strategy is to prove the Haskell version correct; then prove the C version matches the Haskell version. However, I don't think this is right. By my understanding of the paper, the Haskell implementation isn't proven to be correct, it's more of a prototyping tool. The Haskell version is used as an intermediate representation that can be automatically translated into Isabelle/HOL and quickly proven to have various properties. If the proofs don't work at this level, it's easy to change, re-translate, and re-check. To make it easily tramslatable to Isabelle/HOL, they forego many Haskell features, such as typeclasses, or making use of laziness. The Haskell program is also designed to match the eventual C implementation, so it's using C-like data types, pointers, etc - not native Haskell data structures,nor making use of the Haskell GC. The proofs achieved at this level apply to the auto-generated Isabelle/HOL translation of the Haskell code. The Haskell runtime is not modeled here in any way, and as such the proofs do not hold for the Haskell executable code that you can run on the simulator. The Haskell prototype was then translated manually to C, trying to keep as close to a 1:1 translation as possible, while still allowing various micro-optimizations. Then, the exact C code was manually translated back to Isabelle/HOL, where they also had a complete model of the semantics of every C statement that they used (they use a subset of C, with the biggest missing feature being references to local variables - you can't use &x if x is a local variable in their C code). Isabelle/HOL was then used to check that this manually written implementation implemented the abstract specification with all of the proven guarantees. So, the Haskell part was ultimately a convenience, not a fully necessary part of the proof (though the whole thing would probably not have been feasible had they not used it). It was a decent middle ground between being possible for the kernel devs to define the code in it, and the formal verification guys to translate it to Isabelle and verify it. If they had tried to write the C code directly, the cost of translating any change to the C code back to Isabelle for verification would have been too high. Conversely, having the kernel devs learn enough Isabelle to define the prototype code directly in Isabelle would have also been too complicated as well - and I believe the Isabelle code could not be easily executed to be able to do more regular debugging on it during the development process, the way the Haskell code could be run on the simulator. [0] https://www.sigops.org/s/conferences/sosp/2009/papers/klein-sosp09.pdf https://www.sigops.org/s/conferences/sosp/2009/papers/klein-...
js8 1y ago
I wish but the opposite seems to be coming - Haskell will have less support from coding AIs than mainstream languages. I think people, who care about FP, should think about what is appealing about coding in natural language and is missing from programming in strongly typed FP languages such as Haskell and Lean. (After all, what attracted me to Haskell compared to Python was that the typechecking is relatively cheap thanks to type inference.) I believe that natural language in coding has allure because it can express the outcome in fuzzy manner. I can "handwave" certain parts and the machine fills them out. I further believe, to make this work well with formal languages, we will need to use some kind of fuzzy logic, in which we specify the programs. (I particularly favor certain strong logics based on MTL but that aside.) Unfortunately, this line of research seems to have been pretty much abandoned in AI in favor of NNs.
Paradigma11 1y ago
I used a LSP MCP tool for a LLM and was so far a bit underwhelmed. The problem is that LSP is designed for human consumption and LLMs have different constraints. LLMs don't use the LSP exploratory to learn the API, you just give it to it as a context or MCP tool. LLMs are really good at pattern matching and wont make type errors as long as the type structure and constructs are simple. If they are not simple it is not said that the LLM can solve and the user understand it.
agent281 1y ago
IMO, Haskell is less helpful for an LLM because of its advanced language features. The LLM is reasoning about the language textually. Since Haskell is very tense, the LLM would need a very strong model of how the language works. I think languages with more minimal features and really good compile time errors would work well with LLMs. In particular, I've heard multiple people say how good LLMs are at generating Go. Personally, I like languages with type inference so this wouldn't be my preference.

seanmcdirmid 1y ago

We might see wider adoption of dependently typed languages like Agda. But limited corpus might become the limiting factor, I’m not sure how knowledge transfers as the languages get more different.

ipnon 1y ago
It's getting cheaper and cheaper to generate corpora by the day, and Agda has the advantage of being verifiable like Lean. So you can simulate large amounts of programs and feed these back into the model. I think this is a major reason why we're seeing remarkable improvements in formal sciences like the recent IMO golds, and yet LLMs are still struggling to generate aesthetically pleasing and consistent CSS. Imagine a high schooler who can win an IMO gold medal but can't center a div!
- andrewflnr 1y ago
  It seems like "generating" a corpus in that situation is more like a search process guided by prompts and more critically the type checker, rather than a straight generation process right? You need some base reality or you'll still just have garbage in, garbage out.

tsimionescu 1y ago

> can be formally verified using well known algos Is there any large formally verified project written in Haskell? The most well known ones are C (seL4 microkernel) and Coq+OCaml (CompCert verified C compiler).

aetherspawn 1y ago
Well, Haskell has GADTs, new type wrappers and type interfaces which can be (and are often) used to implement formal verification using meta programming, so I get the point he was making. You pretty much don’t need to plug another language into Haskell to be satisfied about certain conditions if the types are designed correctly.
- tsimionescu 1y ago
  Those can all encode only very simplistic semantics of the code. You need either a model checker or dependent types to actually verify any kind of interesting semantics (such as "this sort function returns the number in a sorted order", or "this monad obeys the monad laws"). GADTs, newtypes and type interfaces are not significantly more powerful than what you'd get in, say, a Java program in terms of encoding semantics into your types. Now, I believe GHC also has support for dependent types, but the question stands: are there any major Haskell projects that actually use all of these features to formally verify their semantics? Is any part of the Haskell standard library formally verified, for example? And yes, I do understand that type checking is a kind of formal verification, so in some sense even a C program is "formally verified", since the compiler ensures that you can't assign a float to an int. But I'm specifically asking about formal verification of higher level semantics - sorting, monad laws, proving some tree is balanced, etc.
gizmo686 1y ago
seL4 has a Haskell implementation. It only runs under a simulator (as opposed to on real hardware). Their main proof strategy is to prove the Haskell version correct; then prove the C version matches the Haskell version.
- tsimionescu 1y ago
  I admit that I was not aware of their use of Haskell, so thanks for bringing this up! It motivated me to go and actually read (parts of) their paper [0]. > Their main proof strategy is to prove the Haskell version correct; then prove the C version matches the Haskell version. However, I don't think this is right. By my understanding of the paper, the Haskell implementation isn't proven to be correct, it's more of a prototyping tool. The Haskell version is used as an intermediate representation that can be automatically translated into Isabelle/HOL and quickly proven to have various properties. If the proofs don't work at this level, it's easy to change, re-translate, and re-check. To make it easily tramslatable to Isabelle/HOL, they forego many Haskell features, such as typeclasses, or making use of laziness. The Haskell program is also designed to match the eventual C implementation, so it's using C-like data types, pointers, etc - not native Haskell data structures,nor making use of the Haskell GC. The proofs achieved at this level apply to the auto-generated Isabelle/HOL translation of the Haskell code. The Haskell runtime is not modeled here in any way, and as such the proofs do not hold for the Haskell executable code that you can run on the simulator. The Haskell prototype was then translated manually to C, trying to keep as close to a 1:1 translation as possible, while still allowing various micro-optimizations. Then, the exact C code was manually translated back to Isabelle/HOL, where they also had a complete model of the semantics of every C statement that they used (they use a subset of C, with the biggest missing feature being references to local variables - you can't use &x if x is a local variable in their C code). Isabelle/HOL was then used to check that this manually written implementation implemented the abstract specification with all of the proven guarantees. So, the Haskell part was ultimately a convenience, not a fully necessary part of the proof (though the whole thing would probably not have been feasible had they not used it). It was a decent middle ground between being possible for the kernel devs to define the code in it, and the formal verification guys to translate it to Isabelle and verify it. If they had tried to write the C code directly, the cost of translating any change to the C code back to Isabelle for verification would have been too high. Conversely, having the kernel devs learn enough Isabelle to define the prototype code directly in Isabelle would have also been too complicated as well - and I believe the Isabelle code could not be easily executed to be able to do more regular debugging on it during the development process, the way the Haskell code could be run on the simulator. [0] https://www.sigops.org/s/conferences/sosp/2009/papers/klein-sosp09.pdf https://www.sigops.org/s/conferences/sosp/2009/papers/klein-...

js8 1y ago

I wish but the opposite seems to be coming - Haskell will have less support from coding AIs than mainstream languages. I think people, who care about FP, should think about what is appealing about coding in natural language and is missing from programming in strongly typed FP languages such as Haskell and Lean. (After all, what attracted me to Haskell compared to Python was that the typechecking is relatively cheap thanks to type inference.) I believe that natural language in coding has allure because it can express the outcome in fuzzy manner. I can "handwave" certain parts and the machine fills them out. I further believe, to make this work well with formal languages, we will need to use some kind of fuzzy logic, in which we specify the programs. (I particularly favor certain strong logics based on MTL but that aside.) Unfortunately, this line of research seems to have been pretty much abandoned in AI in favor of NNs.

Paradigma11 1y ago

I used a LSP MCP tool for a LLM and was so far a bit underwhelmed. The problem is that LSP is designed for human consumption and LLMs have different constraints. LLMs don't use the LSP exploratory to learn the API, you just give it to it as a context or MCP tool. LLMs are really good at pattern matching and wont make type errors as long as the type structure and constructs are simple. If they are not simple it is not said that the LLM can solve and the user understand it.

agent281 1y ago

IMO, Haskell is less helpful for an LLM because of its advanced language features. The LLM is reasoning about the language textually. Since Haskell is very tense, the LLM would need a very strong model of how the language works. I think languages with more minimal features and really good compile time errors would work well with LLMs. In particular, I've heard multiple people say how good LLMs are at generating Go. Personally, I like languages with type inference so this wouldn't be my preference.