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 Raymond on 2024-11-11 at 17:07

@jonmsterling @rahulc29 Thats a great point. I think the lack of ecosystem is one of the biggest impediment to adoption for agda and idris. Getting used to "oh, there's a library for that" is really really nice. And it could kill a project if you suddenly realize you need to write an entire library from scratch. Many place can't justify that investment.

So here's to hoping some tech giant picks up a dependently typed language (please don't make it lean lol)

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

Written by Jon Sterling on 2024-11-11 at 17:15

@isAdisplayName @rahulc29 Yeah :)

Well, honestly, it’s going to be Lean. I think we dependent type theorists have been a little reluctant to push for our work to go mainstream, because once you do this you can’t turn back and many mistakes get locked in for years or even decades. This is, I suppose, what is happening with Lean — which is simultaneously a huge win and a huge loss for type theory. (Mostly a win, IMO, but there are a number of cultural ideas embedded in the Lean project that I think are very harmful.)

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

Written by Nathan Corbyn on 2024-11-11 at 17:42

@jonmsterling @isAdisplayName @rahulc29 can you give some examples of the harmful ideas?

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

Written by Jon Sterling on 2024-11-11 at 18:04

@antidote @isAdisplayName @rahulc29 I think the big one is "Equality is proved by tactics anyway, so there is no need to ensure that definitional equality has any global properties whatsoever". This leads to bad technical conclusions, like "It is OK that definitional equality is not transitive, you use 'simp' instead and nobody expects 'simp' to be able to reason transitively anyway".

This harmful idea is related to another harmful idea embedded in the project, namely "We don't need no stinkin', pointy-headed type theorists”.

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

Written by Philippa Cowderoy on 2024-11-11 at 18:50

@jonmsterling @antidote @isAdisplayName @rahulc29 I guess there's going to be a big opportunity in 20-30 years' time. Problem is you'd have to start work 10-15 years ahead of the opportunity unless we can figure out how to build tools we can share across projects.

=> More informations about this toot | More toots from flippac@types.pl

Written by Jon Sterling on 2024-11-11 at 21:49

@flippac @antidote @isAdisplayName @rahulc29 I think you may be right... But we also have to be sure that we don't end up like Standard ML — chasing after everyone reminding them about how we did it right first, but being ignored. Honestly I think that is a very real possibility...

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

Toot

Written by Conor Mc Bride on 2024-11-11 at 22:55

@jonmsterling @flippac @antidote @isAdisplayName @rahulc29 I have the receipts. It's not a possibility.

=> More informations about this toot | More toots from pigworker@types.pl

Descendants