3 ms·
> What are the deficiencies of Haskell in this area, to your mind? So I knew a wizzy haskell programmer, who repeatedly did the following. They'd deeply under
by mncharity 4y ago
> What are the deficiencies of Haskell in this area, to your mind?
So I knew a wizzy haskell programmer, who repeatedly did the following. They'd deeply understand the mathematics of some problem domain. Use Coq to explore, analyze, and find a solution approach. Design a haskell model to support it. Extend ghc internals to permit that model. And then mentally compile a domain solution down to haskell. Oh, yeah, and the haskell compiler would then emit binary.
Through much of that, the haskell compiler isn't helping. It's serving as an inconveniently inexpressive intermediate representation, the backend target for a wizzy wetware compiler. I so very can't do that - just no way. I'd need a language and compiler which can collaborate with me much more extensively, far earlier in the process. One with which I can describe and discuss the problem domain.
I want to be able to say, drat, looks like I'm stuck yet again implementing another bloody 2D graphics like thing... Ok, give me a bounded discrete affine space over numeric tuples with all the trimmings. And for the implementation type, lets start in with this set of cache-aware tradeoffs. Ok, maybe that will satisfice. Moving on...
I'd like a language which supports a pushout lattice of theories. Given a theory, add a couple of types, operators, or laws, added in any order, and you get to the same theory. Permitting programming which feels like math. Not years of committee discussion to make monads applicative. I don't even need Agda-style "let's prove the world" - I'm mostly ok with Ruby-style "tests are green so it's all good". But I really want to be able to express problem domains, and to work collaboratively with tooling to craft solutions. And that's not (yet?) haskell.
- nine_k 4y agoWow, that's insightful.
- mncharity 4y ago:) Decades of frustration, and some fun conversations with good people. Credit for the "pushout lattice of theories" characterization to one - "sounds like what you want is a ...". Wish I knew how to nudge progress faster. Late 1980's "seems clear I want something X-flavored, and with so much related work, we'll be there soon!" became "progress is sooo slow and diffuse". Became "I still hope to dance code before I die". Became "oh well, not looking likely". Or how to avoid burnout on moonshot spikes... or...