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
@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
@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
@isAdisplayName @chrisamaphone you're gonna LOVE idris! https://github.com/idris-lang/Idris2/
=> More informations about this toot | More toots from rahulc29@mathstodon.xyz
@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
@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
@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
@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
@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
@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
@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
@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
@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
@jonmsterling @isAdisplayName @rahulc29 can you give some examples of the harmful ideas?
=> More informations about this toot | More toots from antidote@mathstodon.xyz
@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
@antidote @isAdisplayName @rahulc29 I think it is kind of sad, because in the mists of time (among committees and contributors who are now forgotten), Lean was conceived as a way to start fresh and correct the mistakes of Coq that were too hard to correct in an existing project. I do not know exactly what happened in between the early (contentious, from what I've heard) days of the project and the time when Lean's outwardly visible history began, but it seems that the direction of the project ended up being more to fix a lot of usability problems with Coq (very good!) but introduce and adhere tightly to a whole range of new technical design bugs that (1) are avoidable, and (2) do cause usability problems, but the responsibility for this problems is conveniently laundered so as to make users think it is their fault rather than the tool's fault.
=> More informations about this toot | More toots from jonmsterling@mathstodon.xyz
@antidote @isAdisplayName @rahulc29 Since I've said some negative things, let me say some positive things about Lean.
The tooling is simply amazing, and it is getting better and better. The libraries (like mathlib) are really impressive. A huge cultural improvement introduced by Lean over Coq is to prioritise a system where you can do classical mathematics without friction. (It's of course possible in Coq, but you have to step through all these bizarre French Constructivist nomenclatures and mistaken or archaic ideas about constructivity, etc...)
=> More informations about this toot | More toots from jonmsterling@mathstodon.xyz
@jonmsterling @antidote @isAdisplayName what does it mean for Lean's definitional equality to not be transitive? Lean's implementation violates transitivity of definitional equality?
=> More informations about this toot | More toots from rahulc29@mathstodon.xyz
@rahulc29 @antidote @isAdisplayName Ah yes, thanks for the clarification.
=> More informations about this toot | More toots from jonmsterling@mathstodon.xyz
@jonmsterling @antidote @isAdisplayName it is pretty counter intuitive in my opinion. To my knowledge, one checks for definitional equality by normalising and then checking equality of normal forms. Does Lean not do that in its kernel? Or is there some known bug in the normalisation function that the community has deemed not-a-priority (presumably due to tactics etc. working well enough) ?
=> More informations about this toot | More toots from rahulc29@mathstodon.xyz
@rahulc29 @jonmsterling @isAdisplayName my little experience with Lean (the last three weeks of working on a formalisation) gave little hint of any normalising going on—even when I really wanted it!
=> More informations about this toot | More toots from antidote@mathstodon.xyz
@antidote @rahulc29 @jonmsterling @isAdisplayName
The working lean philosophy (well... maybe "vibe" is a better word) seems to be that you should not reduce when you can rewrite. More precisely, the goal is to keep the definition dependent aspects of a proof confined to API lemmas and rely on those lemmas for other proofs. It has the benefit that changes to default configurations around normalisation that happens from time to time only affect the API lemmas.
=> More informations about this toot | More toots from escape_velocity@functional.cafe
@rahulc29 @antidote @isAdisplayName Well, in practice you implement some algorithm that is equivalent to the one you describe, but is more efficient. The problem with Lean is, to my recollection, that the definitional equality relation is very strong and includes things where you would have to invent out of thin air a proof of some proposition. When this theory is turned into an algorithm, there could be many potential impacts; for lean, I seem to recall that the impact is that there are equations that can be proved by sequencing two “refls” but not by using a single “refl”. Syntactically minded people identify this as a failure of subject reduction, but I think that description can obscure the practical impact.
=> More informations about this toot | More toots from jonmsterling@mathstodon.xyz
@rahulc29 @antidote @isAdisplayName There are two instances of this problem in Lean, one easy to fix (or maybe already fixed?) and one harder to fix now without impacting a lot of library code. The latter is the ability to do recursion on proofs of proof irrelevant inductive propositions; if it was required to be proof relevant, the problem would disappear. But I think it can be hard to make this change, when considering the potential impacts on Lean code in the wild.
=> More informations about this toot | More toots from jonmsterling@mathstodon.xyz
@rahulc29 @jonmsterling @antidote @isAdisplayName
The root cause is Lean allowing subsingleton elimination of inductive propositions (including the prop-valued accessibility predicate).
The ideal definitional equality that respects transitivity (and other nice properties) in this setting is undecidable, so any implementation inherently has to be broken somehow (see section 3.1 of https://github.com/digama0/lean-type-theory/releases for an example).
=> More informations about this toot | More toots from LordQuaggan@hachyderm.io
@LordQuaggan @rahulc29 @antidote @isAdisplayName Ah, thanks for linking to Mario’s thesis. He has done a careful analysis of these issues.
=> More informations about this toot | More toots from jonmsterling@mathstodon.xyz
@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
@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
@jonmsterling @antidote @isAdisplayName @rahulc29 I suspect Idris is a good indicator of one way to avoid it: being the Haskell to eg Agda's SML in the programming space will sooner or later give mathematicians reasons to look at a language that could safely coexist with Lean so long as it can get off its own ground.
(Besides, much as SML did a lot, it also ended up being a little stagnant for ongoing meta-level research in a way I don't think Agda is likely to be - which is why Ocaml and Haskell got more mindshare amongst people who wanted to do things)
=> More informations about this toot | More toots from flippac@types.pl
@jonmsterling @antidote @isAdisplayName @rahulc29 I think it's also worth mentioning that the academic side of the Haskell community did a huge amount of active ignoring/failing to cite over the years and that did a lot of damage (including to members who went on to do further research)
=> More informations about this toot | More toots from flippac@types.pl
@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
@isAdisplayName @chrisamaphone what is the "level" of dependently typing you would like ?Is it really Coq/lean/and level? More Idris like ? Just having value directed types constraints?
If the latter, I use Scala, a production ready dependently typed language - but not sure it's what you have in mind?
I can write things like that in Scala:
val y: Int :| Greater[5] = 3 //Compile-time error: Should be greater than 5
=> More informations about this toot | More toots from fanf42@treehouse.systems
@chrisamaphone @isAdisplayName I don't think the PR campaign would exist if we just had a wealth of funding to research what we wanted. But funding is scarce and competitive and we have other parts of computer science claiming they're about to solve general AI
Like the committee for Canada's main science grants have zero PL people on it. Thankfully they get external reviews.
=> More informations about this toot | More toots from joey@mathstodon.xyz This content has been proxied by September (3851b).Proxy Information
text/gemini