5 ms·

For a long time already I've wanted to make the leap towards learning dependently typed programming, but I was never sure which language to invest in - they all

For a long time already I've wanted to make the leap towards learning dependently typed programming, but I was never sure which language to invest in - they all seemed either very focused on just proofs (Coq, Lean) or just relatively far from Haskell in terms of maturity (Agda, Idris). I went through Software Foundations [0] (Coq) which was fun and interesting but I can't say I ever really applied what I used there in software (I did get more comfortable with induction proofs). You're mentioning Lean with Agda and Idris - is Lean usable as a general purpose language? I've been curious about Lean but I got the impression it sort of steps away from Haskell's legacy in terms of syntax and the like (unlike Agda and Idris) so was concerned it would be a large investment and wouldn't add much to what I've learned from Coq. I'd love any insights on what's a useful way to learn more in the area of dependent types for a working engineer today. [0] https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/

iso8859-1 2y ago
Lean aims to be a general purpose language, but I haven't seen people actually write HTTP servers in it. If Leo de Moura really wanted it to be general purpose, what does the concurrent runtime look like then? To my knowledge, there isn't one? That's why I've been writing an HTTP server in Idris2 instead. Here's a todo list demo app[1] and a hello world demo[2]. The advantage of Idris is that it compiles to e.g. Racket, a high level language with a concurrent runtime you can bind to from Idris. It's also interesting how languages don't need their own hosting (e.g. Hackage) any more. Idris packages are just listed in a TOML file[3] (like Stackage) but still hosted on GitHub. No need for versions, just use git commit hashes. It's all experimental anyway. [1]: https://janus.srht.site/docs/todolist.html https://janus.srht.site/docs/todolist.html [2]: https://git.sr.ht/~janus/web-server-racket-hello-world/tree/master/item/src/HelloWorld.idr https://git.sr.ht/~janus/web-server-racket-hello-world/tree/... [3]: https://github.com/stefan-hoeck/idris2-pack-db/blob/main/STATUS.md https://github.com/stefan-hoeck/idris2-pack-db/blob/main/STA...
- drzzhan 2y ago
  This is not related to Lean or Haskell. I'm just wondering why when people are curious about a new general-purpose language, the first thing they test is an HTTP server.
- ants_everywhere 2y ago
  > (like Stackage) but still hosted on GitHub I don't have much experience with Haskell, but one of the worst experiences has been Stack's compile time dependency on GitHub. GitHub rate limits you and builds take forever.
  - tome 2y ago
    That's interesting. Could you say more? This is something that we (speaking as part of the Haskell community) should fix. As far as I know Stack/Stackage should pick up packages from Hackage. What does it use GitHub for?
    - ants_everywhere 2y ago
      I'm not entirely sure where it uses GitHub and where Hackage, but there are a few GitHub issues on the Stack repo about it: - Binary upgrade of Stack fails due to GitHub API request limit #4979 (https://github.com/commercialhaskell/stack/issues/4979 https://github.com/commercialhaskell/stack/issues/4979) - GitHub rate limiting can affect Stack CI #6034 (https://github.com/commercialhaskell/stack/issues/6034 https://github.com/commercialhaskell/stack/issues/6034) And a few more. The "fix" is having Stack impersonate the user (https://github.com/commercialhaskell/stack/pull/6036 https://github.com/commercialhaskell/stack/pull/6036) and authenticate to the API. This unblocks progress, but this is really a design bug and not something I think people should emulate. Every other language I've used allows you to build code without authenticating to a remote service.
      - tome 2y ago
        Thanks! So it seems to be not packages, but templates, and this comment suggests it wasn't GitHub doing the rate limiting after all: https://github.com/commercialhaskell/stack/issues/4979#issuecomment-1603388213 https://github.com/commercialhaskell/stack/issues/4979#issue... > Every other language I've used allows you to build code without authenticating to a remote service. Sure, the problem here wasn't "building". It was downloading a package template (which one doesn't tend to do 60 times per hour). I agree packages shouldn't be fetched from GitHub.
- orbifold 2y ago
  There are tasks, which are implemented as part of the runtime and they appear to plan to integrate libuv in the future. Some of the runtime seems to be fairly easy to hack and have somewhat nice ways of interoperating with both C, C++ and Rust.
agentultra 2y ago
Lean can be used to write software in [0]. I dare say that it may even be the intended use for Lean 4. Work on porting mathlib to Lean 4 is far along and the mathematicians using it will certainly continue to do so. However there is more space for software written in Lean 4 as well. However... it's no where near ready for production use. They don't care about maintaining backwards compatibility. They are more focused on getting the language itself right than they are about helping people build and maintain software written in it. At least for the foreseeable future. If you do build things in it you're working on shifting ground. But it has a lot of potential. The C code generated by Lean 4 is good. Although, that's another trade-off: compiling to C is another source of "quirks." [0] https://agentultra.github.io/lean-4-hackers/ https://agentultra.github.io/lean-4-hackers/
- staunton 2y ago
  > Work on porting mathlib to Lean 4 is far along As far as I understand, that work is in fact done.
mebassett 2y ago
Lean definitely intends to be usable as a general purpose language someday. but I think the bulk of the people involved are more focused on automated theorem proving. The Lean FRO [0] has funds to guide development of the language and they are planning to carve out a niche for stuff that requires formal verification. I'd say in terms of general purpose programming it fits into the category of being "relatively far from haskell in terms of maturity". [0] https://lean-fro.org/about/roadmap-y2/ https://lean-fro.org/about/roadmap-y2/
pmarreck 2y ago
One reason I took interest in Idris (and lately Roc, although it's even less mature) is the promise of a functional but usable to solve problems today language with all the latest thinking on writing good code baked-in already, compiling to a single binary (something I always envied about Go, although unfortunately it's Go). There simply isn't a lot there yet in the space of "pure functional language with only immutable values and compile time type checking that builds a single fast binary (and has some neat developer-friendly features/ideas such as dependent types, Roc's "tags" or pattern-matching with destructuring)" (this rules out OCaml, for example, despite it being mature). You get a lot of that, but not all of it, with other options (OCaml, Elixir/Erlang, Haskell... but those 3 offer a far larger library of ready-to-import software at this point). Haskell did manage to teach everyone who cares about these things that managing side-effects and keeping track of "purity" is important. But it's frankly still early-days and we're still far from nirvana; Rust is starting to show some warts (despite still being a massive improvement over C from a safety perspective), and people are looking around for what's next. One barely-touched thing is that there are compiler optimizations made possible by pure functional/pure immutable languages (such as caching a guaranteed result of an operation where those guarantees simply can't be given elsewhere) that have simply been impossible until now. (Roc is trying to go there, from what I can tell, and I'm here for it! Presumably, Rust has already, as long as you stick with its functional constructs, which I hear is hard sometimes)
- staunton 2y ago
  > Rust is starting to show some warts (despite still being a massive improvement over C from a safety perspective) The way it seems to me is that actually Rust aims to be an improvement over C++ rather than C. (And Zig aims to be an improvement over C rather than C++.) The major downsides of both will be the same as their reference point: Rust will eventually be too complicated for anyone to understand while still not being really safe (and the complexity then comes back to bite you one more time). Zig will be easy to understand and use but too unsafe to use for important applications (at least once people start really caring about software in important applications). Both of these will be fairly niche because compiling to a single binary just isn't as important, as elegant as it might be.
bmitc 2y ago
When I last looked into Lean, I was highly unimpressed, even for doing math proofs. There's no way I'd invest into as a general-purpose language. Idris at least does state that they what people building real programs with it and don't want it to just be a research language. For dependent types, I myself am skeptical about languages trying to continuously push more and more stuff into types. I am not certain that such efforts are a net positive on writing good software. By their very definition, the more typed a language gets, the less programs it can represents. That obviously reduces buggy programs, but it also reduces non-buggy programs that you can implement. Highly typed languages force more and more effort into pre-compile time and you will often find yourself trying to fit a problem into the chains of the type system. Rather, I think reasonably multi-paradigm languages like F# are the sweet spot. Just enough strict typing and functional core to get you going for most of your program, but then it allows classes and imperative programming when those paradigms are appropriate. I think the way to go to write better software is better tooling and ergonomics. I don't think type systems are going to magically save us.
- tsimionescu 2y ago
  > By their very definition, the more typed a language gets, the less programs it can represents. That obviously reduces buggy programs, but it also reduces non-buggy programs that you can implement. While I generally share your skepticism, I think this is quite wrong. A good part of the point of advanced type systems is to make more complex problems possible while still being well typed. For example, in C, if you want a function whose return type is tied to an input argument's type, you either use void* and casts (no type safety), or you don't write that function. In languages with even slightly more advanced type systems, you can write that function and still get full type safety. Even more advanced type systems achieve the same things: you can take programs that can only be written in a simpler type system and make them safe. In standard Haskell, for example, you can't write a Monad and actually have the compiler check that it respects the Monad laws - the implementation of Monad functions just assumes that any type that implements the right shape of functions will work as a monad. With dependent types, you can actually enforce that functions designed to work with monads only apply to types that actually respect the monad laws. The trade-off with very complex type systems is different, in my opinion: after some point, you start duplicating your program's logic, once in the implentation code, but again in the type signatures. For example, if you want to specify that a sort function actually sorts the input list, you might find that the type specification ends up not much shorter than the actual code of the function. And apart from raw effort, this means that your type specifications start being large enough that they have their own bugs.
saghm 2y ago
I took that course as well, and for me, the big takeaway wasn't that I specifically want to use Coq for anything practical, but the idea that you can actually do quite a lot with a non-Turing complete language. Realizing that constraints in a language can be an asset rather than a limitation is something that I think isn't as widely understood as it should be.

iso8859-1 2y ago

Lean aims to be a general purpose language, but I haven't seen people actually write HTTP servers in it. If Leo de Moura really wanted it to be general purpose, what does the concurrent runtime look like then? To my knowledge, there isn't one? That's why I've been writing an HTTP server in Idris2 instead. Here's a todo list demo app[1] and a hello world demo[2]. The advantage of Idris is that it compiles to e.g. Racket, a high level language with a concurrent runtime you can bind to from Idris. It's also interesting how languages don't need their own hosting (e.g. Hackage) any more. Idris packages are just listed in a TOML file[3] (like Stackage) but still hosted on GitHub. No need for versions, just use git commit hashes. It's all experimental anyway. [1]: https://janus.srht.site/docs/todolist.html https://janus.srht.site/docs/todolist.html [2]: https://git.sr.ht/~janus/web-server-racket-hello-world/tree/master/item/src/HelloWorld.idr https://git.sr.ht/~janus/web-server-racket-hello-world/tree/... [3]: https://github.com/stefan-hoeck/idris2-pack-db/blob/main/STATUS.md https://github.com/stefan-hoeck/idris2-pack-db/blob/main/STA...

drzzhan 2y ago
This is not related to Lean or Haskell. I'm just wondering why when people are curious about a new general-purpose language, the first thing they test is an HTTP server.
ants_everywhere 2y ago
> (like Stackage) but still hosted on GitHub I don't have much experience with Haskell, but one of the worst experiences has been Stack's compile time dependency on GitHub. GitHub rate limits you and builds take forever.
- tome 2y ago
  That's interesting. Could you say more? This is something that we (speaking as part of the Haskell community) should fix. As far as I know Stack/Stackage should pick up packages from Hackage. What does it use GitHub for?
  - ants_everywhere 2y ago
    I'm not entirely sure where it uses GitHub and where Hackage, but there are a few GitHub issues on the Stack repo about it: - Binary upgrade of Stack fails due to GitHub API request limit #4979 (https://github.com/commercialhaskell/stack/issues/4979 https://github.com/commercialhaskell/stack/issues/4979) - GitHub rate limiting can affect Stack CI #6034 (https://github.com/commercialhaskell/stack/issues/6034 https://github.com/commercialhaskell/stack/issues/6034) And a few more. The "fix" is having Stack impersonate the user (https://github.com/commercialhaskell/stack/pull/6036 https://github.com/commercialhaskell/stack/pull/6036) and authenticate to the API. This unblocks progress, but this is really a design bug and not something I think people should emulate. Every other language I've used allows you to build code without authenticating to a remote service.
    - tome 2y ago
      Thanks! So it seems to be not packages, but templates, and this comment suggests it wasn't GitHub doing the rate limiting after all: https://github.com/commercialhaskell/stack/issues/4979#issuecomment-1603388213 https://github.com/commercialhaskell/stack/issues/4979#issue... > Every other language I've used allows you to build code without authenticating to a remote service. Sure, the problem here wasn't "building". It was downloading a package template (which one doesn't tend to do 60 times per hour). I agree packages shouldn't be fetched from GitHub.
orbifold 2y ago
There are tasks, which are implemented as part of the runtime and they appear to plan to integrate libuv in the future. Some of the runtime seems to be fairly easy to hack and have somewhat nice ways of interoperating with both C, C++ and Rust.

agentultra 2y ago

Lean can be used to write software in [0]. I dare say that it may even be the intended use for Lean 4. Work on porting mathlib to Lean 4 is far along and the mathematicians using it will certainly continue to do so. However there is more space for software written in Lean 4 as well. However... it's no where near ready for production use. They don't care about maintaining backwards compatibility. They are more focused on getting the language itself right than they are about helping people build and maintain software written in it. At least for the foreseeable future. If you do build things in it you're working on shifting ground. But it has a lot of potential. The C code generated by Lean 4 is good. Although, that's another trade-off: compiling to C is another source of "quirks." [0] https://agentultra.github.io/lean-4-hackers/ https://agentultra.github.io/lean-4-hackers/

staunton 2y ago
> Work on porting mathlib to Lean 4 is far along As far as I understand, that work is in fact done.

mebassett 2y ago

Lean definitely intends to be usable as a general purpose language someday. but I think the bulk of the people involved are more focused on automated theorem proving. The Lean FRO [0] has funds to guide development of the language and they are planning to carve out a niche for stuff that requires formal verification. I'd say in terms of general purpose programming it fits into the category of being "relatively far from haskell in terms of maturity". [0] https://lean-fro.org/about/roadmap-y2/ https://lean-fro.org/about/roadmap-y2/

pmarreck 2y ago

One reason I took interest in Idris (and lately Roc, although it's even less mature) is the promise of a functional but usable to solve problems today language with all the latest thinking on writing good code baked-in already, compiling to a single binary (something I always envied about Go, although unfortunately it's Go). There simply isn't a lot there yet in the space of "pure functional language with only immutable values and compile time type checking that builds a single fast binary (and has some neat developer-friendly features/ideas such as dependent types, Roc's "tags" or pattern-matching with destructuring)" (this rules out OCaml, for example, despite it being mature). You get a lot of that, but not all of it, with other options (OCaml, Elixir/Erlang, Haskell... but those 3 offer a far larger library of ready-to-import software at this point). Haskell did manage to teach everyone who cares about these things that managing side-effects and keeping track of "purity" is important. But it's frankly still early-days and we're still far from nirvana; Rust is starting to show some warts (despite still being a massive improvement over C from a safety perspective), and people are looking around for what's next. One barely-touched thing is that there are compiler optimizations made possible by pure functional/pure immutable languages (such as caching a guaranteed result of an operation where those guarantees simply can't be given elsewhere) that have simply been impossible until now. (Roc is trying to go there, from what I can tell, and I'm here for it! Presumably, Rust has already, as long as you stick with its functional constructs, which I hear is hard sometimes)

staunton 2y ago
> Rust is starting to show some warts (despite still being a massive improvement over C from a safety perspective) The way it seems to me is that actually Rust aims to be an improvement over C++ rather than C. (And Zig aims to be an improvement over C rather than C++.) The major downsides of both will be the same as their reference point: Rust will eventually be too complicated for anyone to understand while still not being really safe (and the complexity then comes back to bite you one more time). Zig will be easy to understand and use but too unsafe to use for important applications (at least once people start really caring about software in important applications). Both of these will be fairly niche because compiling to a single binary just isn't as important, as elegant as it might be.

bmitc 2y ago

When I last looked into Lean, I was highly unimpressed, even for doing math proofs. There's no way I'd invest into as a general-purpose language. Idris at least does state that they what people building real programs with it and don't want it to just be a research language. For dependent types, I myself am skeptical about languages trying to continuously push more and more stuff into types. I am not certain that such efforts are a net positive on writing good software. By their very definition, the more typed a language gets, the less programs it can represents. That obviously reduces buggy programs, but it also reduces non-buggy programs that you can implement. Highly typed languages force more and more effort into pre-compile time and you will often find yourself trying to fit a problem into the chains of the type system. Rather, I think reasonably multi-paradigm languages like F# are the sweet spot. Just enough strict typing and functional core to get you going for most of your program, but then it allows classes and imperative programming when those paradigms are appropriate. I think the way to go to write better software is better tooling and ergonomics. I don't think type systems are going to magically save us.

tsimionescu 2y ago
> By their very definition, the more typed a language gets, the less programs it can represents. That obviously reduces buggy programs, but it also reduces non-buggy programs that you can implement. While I generally share your skepticism, I think this is quite wrong. A good part of the point of advanced type systems is to make more complex problems possible while still being well typed. For example, in C, if you want a function whose return type is tied to an input argument's type, you either use void* and casts (no type safety), or you don't write that function. In languages with even slightly more advanced type systems, you can write that function and still get full type safety. Even more advanced type systems achieve the same things: you can take programs that can only be written in a simpler type system and make them safe. In standard Haskell, for example, you can't write a Monad and actually have the compiler check that it respects the Monad laws - the implementation of Monad functions just assumes that any type that implements the right shape of functions will work as a monad. With dependent types, you can actually enforce that functions designed to work with monads only apply to types that actually respect the monad laws. The trade-off with very complex type systems is different, in my opinion: after some point, you start duplicating your program's logic, once in the implentation code, but again in the type signatures. For example, if you want to specify that a sort function actually sorts the input list, you might find that the type specification ends up not much shorter than the actual code of the function. And apart from raw effort, this means that your type specifications start being large enough that they have their own bugs.

saghm 2y ago

I took that course as well, and for me, the big takeaway wasn't that I specifically want to use Coq for anything practical, but the idea that you can actually do quite a lot with a non-Turing complete language. Realizing that constraints in a language can be an asset rather than a limitation is something that I think isn't as widely understood as it should be.