Ancestors

Written by Raymond on 2024-11-11 at 01:14

Using haskell as my main language at work is pretty great, except for one thing. Having learned agda first, I got really used to having dependent types at my disposal. Now I often find myself naturally thinking of a solution that makes use of dependent types, then having to translate this solution into haskell. Of course, there is always a translation. But the translation may obfuscate what the code is doing, making it harder for future programmers to understand it and maintain it.

The work I do has no relation to formal verification, nor is it "mission critical" that the code is correct. But I still find my self wishing I could use dependent types, just because they make writing programs and capturing business logic both faster and easier. A language with dependent types requires a less severe translation from the programmers ideas to a compiling program.

=> More informations about this toot | More toots from isAdisplayName@mathstodon.xyz

Written by chris martens on 2024-11-11 at 01:23

@isAdisplayName I can’t stand the PR campaign in programming languages that our stuff is only (or even especially!) good for “mission critical” programming. it’s the human parts that matter

=> More informations about this toot | More toots from chrisamaphone@hci.social

Written by Raymond on 2024-11-11 at 01:54

@chrisamaphone absolutely! Dependent types make a programmer's life better. That's all the justification needed to research them and put energy into implementations.

I really hope the day soon comes when there is widely supported, general purpose language with dependent types. (here I'm counting haskell as a general purpose language)

=> More informations about this toot | More toots from isAdisplayName@mathstodon.xyz

Written by Rahul Chhabra on 2024-11-11 at 07:06

@isAdisplayName @chrisamaphone you're gonna LOVE idris! https://github.com/idris-lang/Idris2/

=> More informations about this toot | More toots from rahulc29@mathstodon.xyz

Written by Raymond on 2024-11-11 at 07:55

@rahulc29 Idris is great! I've bumped up against Idris (and I think Chris has as well). And I love Edwin Brady's book "Type Driven Development in Idris". The language does seem much more geared towards general purpose. But, there is a vast amount of peripheral features and kinks that would need to be worked out before Idris (or any other dependently typed language) can be used in production as a general purpose language.

Even today, large companies using Haskell occasionally have to hire GHC consultants to fix bugs in the compiler or upstream some important feature. When facebook started trying to use haskell at scale, they essentially hired a GHC developer to make the project work.

=> More informations about this toot | More toots from isAdisplayName@mathstodon.xyz

Written by Rahul Chhabra on 2024-11-11 at 08:03

@isAdisplayName i think that's fair, we still cannot use idris in "production". however, it is getting better by the day, so hopefully we can very soon :')

=> More informations about this toot | More toots from rahulc29@mathstodon.xyz

Written by Jon Sterling on 2024-11-11 at 09:42

@rahulc29 @isAdisplayName Yes... And also, I think that there is a pretty huge spectrum of what "production" means to different people. There are some definitions of "production" under which I could certainly use Idris — and ultimately the difficulties would be very similar to those one would encounter in a non-dependently typed language that hasn't had zillions poured into it by Facebook or Google or Apple.

I think in nearly all these cases, what prevents something from being usable "in production" is not so much language features & kinks & compiler bugs, but the lack of an ecosystem.

=> More informations about this toot | More toots from jonmsterling@mathstodon.xyz

Written by Jon Sterling on 2024-11-11 at 09:47

@rahulc29 @isAdisplayName I think there are many problems left to solve in the design & engineering of dependently typed languages. But these gaps are mostly in the area of "How do we enable programmers to effectively use dependent types" — but this is moving the goalposts. One is trying to compare state of the art DT languages with non-DT languages — rather than comparing state of the art DT languages with future/better DT languages, where the improvements are in aspects that are invisible to ordinary non-DT programming.

Relative to the old tech, what we lack is therefore mainly an ecosystem. But ecosystems require investment — which is why Facebook had to hire a GHC engineer, and why Apple made its own language.

=> More informations about this toot | More toots from jonmsterling@mathstodon.xyz

Written by Rahul Chhabra on 2024-11-11 at 09:57

@jonmsterling @isAdisplayName unfortunately, ecosystems development operates on a feedback loop as well, so it is always easier to write a library in a language for which a well-developed ecosystem already exists.

For what it's worth, Idris has one of the best FFIs I've ever used. You can use (almost) any C library "off the shelf".

=> More informations about this toot | More toots from rahulc29@mathstodon.xyz

Written by Jon Sterling on 2024-11-11 at 09:59

@rahulc29 @isAdisplayName yes, that's very true. And ecosystem includes things like a good language server, which probably costs at least a few hundred thousand dollars to build.

=> More informations about this toot | More toots from jonmsterling@mathstodon.xyz

Toot

Written by chris martens on 2024-11-11 at 12:40

@jonmsterling @isAdisplayName @rahulc29 because of the feedback loop nature, though, maybe one of the most critical early parts of the ecosystem is a REPL/web playground/beginner-friendly documentation. getting people excited about the vision is a prerequisite for building it (unless you can pay them)

=> More informations about this toot | More toots from chrisamaphone@hci.social

Descendants