6 ms·

I really look forward to a language with first-class explicit algebras, with operators, laws, equality, types. Rather than ad hocery on multimethods, or kludger

I really look forward to a language with first-class explicit algebras, with operators, laws, equality, types. Rather than ad hocery on multimethods, or kludgery slathered thick over single dispatch, or the ever popular "you just can't get there from here". "1 is not an object; + is not a message"... I'm failing to find the quote, but it dates back like 40 years to smalltalk, and yet here we still are.

drmt 4y ago
Are you thinking about something like AlgebraicJulia, specifically Catlab.jl? It allows to specify Generalized Algebraic Theories and comes with a large list of standard theories. https://algebraicjulia.github.io/Catlab.jl/dev/apis/theories/ https://algebraicjulia.github.io/Catlab.jl/dev/apis/theories... @theory Category{Ob,Hom} begin @op begin (→) := Hom (⋅) := compose end Ob::TYPE Hom(dom::Ob, codom::Ob)::TYPE id(A::Ob)::(A → A) compose(f::(A → B), g::(B → C))::(A → C) ⊣ (A::Ob, B::Ob, C::Ob) (f ⋅ g) ⋅ h == f ⋅ (g ⋅ h) ⊣ (A::Ob, B::Ob, C::Ob, D::Ob, f::(A → B), g::(B → C), h::(C → D)) f ⋅ id(B) == f ⊣ (A::Ob, B::Ob, f::(A → B)) id(A) ⋅ f == f ⊣ (A::Ob, B::Ob, f::(A → B)) end
qsort 4y ago
Wouldn't it become very undecidable very fast going down that route? Programming by defining algebras is interesting idea with many practical applications, even in down-to-earth CRUD apps, but how much magic can you really add before it becomes impossible (or even just very hard) to compile? The closest example in mainstream languages is Haskell, but even there the compiler basically trusts you. Is it possible to add something else while remaining decidable/efficient? I genuinely don't know.
- mncharity 4y ago
  > but even there the compiler basically trusts you Yeah, I'm ok with that. I'm more after expressivity than safety or efficiency. Sometimes they're not separable, but confronted with the usual "we don't know how to efficiently compile that, so we won't allow you to express it", my response is always "the language is not the right level at which to choose such engineering tradeoffs - give me finer-grain control, and in program portions where it matters, I'll trade expressiveness for efficiency or safety... after maybe first trying caching and cloud parallelism and patience and external analysis and ... ".
  - mncharity 4y ago
    > after maybe first trying [...] Oops, I got carried away at the end there. Yes, maximally-restricted tolerable representation buys maximized compiler leverage. But might we more often metaprogram that out of diversely-performant maximal power, rather than bootstrapping it on performant but constraining circumscribed power?
- eru 4y ago
  Haskell already has an extension called UndecidableInstances. Funny enough, even your basic Hindley-Milner style type inference has exponential runtime in the worst case, even if you don't add any bells nor whistles. In practice, people don't tend to write code that triggers that worst-case.
  - bjoli 4y ago
    Am I the only one that likes vanilla Haskell? I find that it quickly becomes messy with all the GHC extensions. I am although more of an SML kind of guy.
    - eru 4y ago
      Many libraries try to stick to Haskell 98. Also whenever someone writes a paper about some new techniques, they always seem to take a lot of pleasure in pointing out when their technique works in Haskell 98. I like that you can mix and match GHC extensions even in the same project. So one library (or even just one module) might use some crazy and messy extensions, but you can still use it from vanilla Haskell. http://dev.stephendiehl.com/hask/#language-extensions http://dev.stephendiehl.com/hask/#language-extensions has a list of extensions and some judgement on them. There are a few that are really neat, but don't really cause any mess: For example, I really like TupleSections. They are not strictly necessary for anything, they are purely cosmetic / syntactic sugar. But they also don't cause any mess. https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/tuple_sections.html https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/tupl... Also: TypedHoles are really neat for developing, and will never show up in your final code. https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/typed_holes.html https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/type...
      - neilparikh 4y ago
        GeneralisedNewtypeDeriving is one that I'd consider fairly important as well.
        eru 4y ago
nine_k 4y ago
What are the deficiencies of Haskell in this area, to your mind?
- 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 ago
    Wow, 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...
TakeBlaster16 4y ago
I'm interested to read more about this if you have any links or want to sketch out a design
- mncharity 4y ago
  A couple of years before covid, Boston Haskell meetup group was active and wizzy. And bar discussion would repeated turn to what a "Haskell-NEXT" might look like. Aside from similar bars at conferences, I've not encountered such discussion elsewhere. Having such discussion work has seemed very sensitive to including extreme outlier quality people. Which very isn't me - I mostly just ask questions. They go home, and even though people left have wizzy math backgrounds and are doing their own language implementations... continuing can be hard. And the costs of such discussion in text, or in zoom... I can't picture that. So... I'm unclear on how progress might be fruitfully nudged. The bottleneck seems waiting for research papers to drop, and existing language efforts to incrementally improve, slowly creeping closer to "oh yeah, we could do that soon". With a big caveat of its been years since I even slightly tried to track the big picture, here are two thoughts on directions which I then felt were getting less attention that I might have liked. First, having wizzy type system power, while not much caring about static typing. I thought of it as sort of a optional-typing CommonLisp attitude. Expressive power, but fine-gain collaborative-compilation tradeoff control over where to pay for what assistance. And second, extremely extensible languages, as can do bulk subsumption of others. So imported modules providing compiler cross-sections, from syntax to type analysis to optimization tweaks. ... Ah well, if humans don't get to it, maybe ML Copilot2030 will give "sure, just express what you want it any mixed mashup of different languages and math, and I'll try guessing what you're trying to say ;) So... I'm unclear on a fruitful way to proceed...? Sorry... I appreciate the thought.
awesomelvin 4y ago
I recently fell in love with Agda and it seems like you'd like it too. It's basically Haskell but even more mathematical, pure, abstract and total.
- mncharity 4y ago
  Agda[1] is fun. Also Idris[2] - more programming language, less proof assistant. [1] https://wiki.portal.chalmers.se/agda/pmwiki.php https://wiki.portal.chalmers.se/agda/pmwiki.php https://github.com/agda/agda https://github.com/agda/agda [2] https://www.idris-lang.org/ https://www.idris-lang.org/
chaxor 4y ago
Does Julia have this quality? I'm not suggesting it does, I'm genuinely curious for anyone that knows this area well.
- mncharity 4y ago
  > Does Julia have this quality? Multiple dispatch, as in Julia, Mathematica, CommonLisp, etc, does get you much closer to this vision than single dispatch. To an extent, but then you're on your own again. Maybe consider compilation as a collaboration of a computer and a wetware compiler. You have knowledge and do analysis which you are unable to share with the computer compiler. For silly tiny illustration, you might know some size variable has to be an integer power of 2, but most language's type systems don't let you tell the compiler that. Or think of writing a datatype in old C - a struct and a bunch of functions. You have a mental model of how they should all hang together, and then you mentally compile that down and hand emit C code and tests. Or you could hand emit assembly code and tests instead. But the C compiler is the more helpful collaborator. You can talk about more (with some sacrifices), and more easily. Now given say two structs and a bunch of associated functions, multiple dispatch allows weaving them together without pains which in single dispatch so discourage weaving. Which is better, but still, you've a couple of structs, a bunch of functions, and a still limited ability to express your intent so the computer compiler can help you with it. So you can have multiple dispatch of + and - , and more easily add new numeric types, but any relationship between + and - is still all in your mind - the compiler has no idea that you think them connected.
- adiM 4y ago
  Yes, Julia has multi-dispatch, which works really well for this type of overloading
  - sundarurfriend 4y ago
    Julia avoids the "ad hocery on multimethods, or kludgery slathered thick over single dispatch", but I'm not sure about "first-class explicit algebras, with operators, laws, equality, types". Would "first-class explicit algebras" involve the language allowing redefining of operator precedences? Julia doesn't allow that. Would it require support for customizable associativity? You can painstakingly do that by defining custom types for every intermediate operation, but it isn't part of base Julia. The original problem in the thread's start, "builtin_object <operator> your_object", is neatly solved by multiple dispatch. But the ask in your grand-parent comment is much bigger, and Julia only has slightly more support for that compared to other languages (i.e. it's a bit less of a pain in the ass to create such algebras, but you'll still have to create it yourself).
deleted 4y ago
[deleted]

drmt 4y ago

Are you thinking about something like AlgebraicJulia, specifically Catlab.jl? It allows to specify Generalized Algebraic Theories and comes with a large list of standard theories. https://algebraicjulia.github.io/Catlab.jl/dev/apis/theories/ https://algebraicjulia.github.io/Catlab.jl/dev/apis/theories... @theory Category{Ob,Hom} begin @op begin (→) := Hom (⋅) := compose end Ob::TYPE Hom(dom::Ob, codom::Ob)::TYPE id(A::Ob)::(A → A) compose(f::(A → B), g::(B → C))::(A → C) ⊣ (A::Ob, B::Ob, C::Ob) (f ⋅ g) ⋅ h == f ⋅ (g ⋅ h) ⊣ (A::Ob, B::Ob, C::Ob, D::Ob, f::(A → B), g::(B → C), h::(C → D)) f ⋅ id(B) == f ⊣ (A::Ob, B::Ob, f::(A → B)) id(A) ⋅ f == f ⊣ (A::Ob, B::Ob, f::(A → B)) end

qsort 4y ago

Wouldn't it become very undecidable very fast going down that route? Programming by defining algebras is interesting idea with many practical applications, even in down-to-earth CRUD apps, but how much magic can you really add before it becomes impossible (or even just very hard) to compile? The closest example in mainstream languages is Haskell, but even there the compiler basically trusts you. Is it possible to add something else while remaining decidable/efficient? I genuinely don't know.

mncharity 4y ago
> but even there the compiler basically trusts you Yeah, I'm ok with that. I'm more after expressivity than safety or efficiency. Sometimes they're not separable, but confronted with the usual "we don't know how to efficiently compile that, so we won't allow you to express it", my response is always "the language is not the right level at which to choose such engineering tradeoffs - give me finer-grain control, and in program portions where it matters, I'll trade expressiveness for efficiency or safety... after maybe first trying caching and cloud parallelism and patience and external analysis and ... ".
- mncharity 4y ago
  > after maybe first trying [...] Oops, I got carried away at the end there. Yes, maximally-restricted tolerable representation buys maximized compiler leverage. But might we more often metaprogram that out of diversely-performant maximal power, rather than bootstrapping it on performant but constraining circumscribed power?
eru 4y ago
Haskell already has an extension called UndecidableInstances. Funny enough, even your basic Hindley-Milner style type inference has exponential runtime in the worst case, even if you don't add any bells nor whistles. In practice, people don't tend to write code that triggers that worst-case.
- bjoli 4y ago
  Am I the only one that likes vanilla Haskell? I find that it quickly becomes messy with all the GHC extensions. I am although more of an SML kind of guy.
  - eru 4y ago
    Many libraries try to stick to Haskell 98. Also whenever someone writes a paper about some new techniques, they always seem to take a lot of pleasure in pointing out when their technique works in Haskell 98. I like that you can mix and match GHC extensions even in the same project. So one library (or even just one module) might use some crazy and messy extensions, but you can still use it from vanilla Haskell. http://dev.stephendiehl.com/hask/#language-extensions http://dev.stephendiehl.com/hask/#language-extensions has a list of extensions and some judgement on them. There are a few that are really neat, but don't really cause any mess: For example, I really like TupleSections. They are not strictly necessary for anything, they are purely cosmetic / syntactic sugar. But they also don't cause any mess. https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/tuple_sections.html https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/tupl... Also: TypedHoles are really neat for developing, and will never show up in your final code. https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/typed_holes.html https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/type...
    - neilparikh 4y ago
      GeneralisedNewtypeDeriving is one that I'd consider fairly important as well.
      - eru 4y ago

nine_k 4y ago

What are the deficiencies of Haskell in this area, to your mind?

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 ago
  Wow, 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...

TakeBlaster16 4y ago

I'm interested to read more about this if you have any links or want to sketch out a design

mncharity 4y ago
A couple of years before covid, Boston Haskell meetup group was active and wizzy. And bar discussion would repeated turn to what a "Haskell-NEXT" might look like. Aside from similar bars at conferences, I've not encountered such discussion elsewhere. Having such discussion work has seemed very sensitive to including extreme outlier quality people. Which very isn't me - I mostly just ask questions. They go home, and even though people left have wizzy math backgrounds and are doing their own language implementations... continuing can be hard. And the costs of such discussion in text, or in zoom... I can't picture that. So... I'm unclear on how progress might be fruitfully nudged. The bottleneck seems waiting for research papers to drop, and existing language efforts to incrementally improve, slowly creeping closer to "oh yeah, we could do that soon". With a big caveat of its been years since I even slightly tried to track the big picture, here are two thoughts on directions which I then felt were getting less attention that I might have liked. First, having wizzy type system power, while not much caring about static typing. I thought of it as sort of a optional-typing CommonLisp attitude. Expressive power, but fine-gain collaborative-compilation tradeoff control over where to pay for what assistance. And second, extremely extensible languages, as can do bulk subsumption of others. So imported modules providing compiler cross-sections, from syntax to type analysis to optimization tweaks. ... Ah well, if humans don't get to it, maybe ML Copilot2030 will give "sure, just express what you want it any mixed mashup of different languages and math, and I'll try guessing what you're trying to say ;) So... I'm unclear on a fruitful way to proceed...? Sorry... I appreciate the thought.

awesomelvin 4y ago

I recently fell in love with Agda and it seems like you'd like it too. It's basically Haskell but even more mathematical, pure, abstract and total.

mncharity 4y ago
Agda[1] is fun. Also Idris[2] - more programming language, less proof assistant. [1] https://wiki.portal.chalmers.se/agda/pmwiki.php https://wiki.portal.chalmers.se/agda/pmwiki.php https://github.com/agda/agda https://github.com/agda/agda [2] https://www.idris-lang.org/ https://www.idris-lang.org/

chaxor 4y ago

Does Julia have this quality? I'm not suggesting it does, I'm genuinely curious for anyone that knows this area well.

mncharity 4y ago
> Does Julia have this quality? Multiple dispatch, as in Julia, Mathematica, CommonLisp, etc, does get you much closer to this vision than single dispatch. To an extent, but then you're on your own again. Maybe consider compilation as a collaboration of a computer and a wetware compiler. You have knowledge and do analysis which you are unable to share with the computer compiler. For silly tiny illustration, you might know some size variable has to be an integer power of 2, but most language's type systems don't let you tell the compiler that. Or think of writing a datatype in old C - a struct and a bunch of functions. You have a mental model of how they should all hang together, and then you mentally compile that down and hand emit C code and tests. Or you could hand emit assembly code and tests instead. But the C compiler is the more helpful collaborator. You can talk about more (with some sacrifices), and more easily. Now given say two structs and a bunch of associated functions, multiple dispatch allows weaving them together without pains which in single dispatch so discourage weaving. Which is better, but still, you've a couple of structs, a bunch of functions, and a still limited ability to express your intent so the computer compiler can help you with it. So you can have multiple dispatch of + and - , and more easily add new numeric types, but any relationship between + and - is still all in your mind - the compiler has no idea that you think them connected.
adiM 4y ago
Yes, Julia has multi-dispatch, which works really well for this type of overloading
- sundarurfriend 4y ago
  Julia avoids the "ad hocery on multimethods, or kludgery slathered thick over single dispatch", but I'm not sure about "first-class explicit algebras, with operators, laws, equality, types". Would "first-class explicit algebras" involve the language allowing redefining of operator precedences? Julia doesn't allow that. Would it require support for customizable associativity? You can painstakingly do that by defining custom types for every intermediate operation, but it isn't part of base Julia. The original problem in the thread's start, "builtin_object <operator> your_object", is neatly solved by multiple dispatch. But the ask in your grand-parent comment is much bigger, and Julia only has slightly more support for that compared to other languages (i.e. it's a bit less of a pain in the ass to create such algebras, but you'll still have to create it yourself).

deleted 4y ago

[deleted]