pikelet-lang / pikelet

A friendly little systems language with first-class types. Very WIP! 🚧 🚧 🚧
https://pikelet-lang.github.io/pikelet/
Apache License 2.0
610 stars 26 forks source link

User-defined infix operators #34

Open brendanzab opened 6 years ago

brendanzab commented 6 years ago

It would be nice to have operators for:

Resources

brendanzab commented 6 years ago

One interesting problem is trying to do precedences in an ok/semi-sane sort-of-way. I think Fortress had something where you could define groups of operators with related precedences. Swift has precedence groups - not sure how that turned out for them. Would you happen to know @graydon?

graydon commented 6 years ago

Hah, I thought for a moment you were soliciting input on whether user defined operators would be a good idea in rust, which I 100% oppose in every conceivable way.

But if you're into it I guess...

The precedence groups themselves don't seem to have been a problem in swift. One thing that is a problem is that operators can, if you're unlucky about how you do name lookup, participate in global name overload resolution and some expensive global type-constraint-solving problems. Makes for some whole-module search and coupling you might not want (a la multimethods). IOW try to just make operators sugar for a member call or at most an already-defined whole-module dispatch mechanism like a typeclass, don't do anything additional for the operators. That was a design mistake on swift's part we're backing off of.

brendanzab commented 6 years ago

Thanks for the info! Might try tracking down some code/libraries that use them to see how it looks. I'd just like to avoid the numeric precedences that are kind of hard to use/visualise in Coq, Agda, and Lean.

Unlike Swift, Pikelet won't have overloading apart from instance arguments (#13), so I'm guessing that would dodge the global name lookup issue? It would kind of look like:

Monoid (a : Type) = Record {
    empty : a,
    append : a -> a -> a,
};

(<>) : {a : Type} {{M : Monoid a}} -> a -> a -> a;
(<>) {{M}} = M.append; 
graydon commented 6 years ago

Shrug it's hard for me to say, I mean, it only really bites us because we have a bad exponential-search problem in expression constraint solving, and any whole-module coupling between files causes whole-module invalidation at the incremental level any time you change a file that uses such a global operator; so both are compile-time costs. Semantically it's no problem.

Whether you can make your implicits system (and compile times) not have those features, well, I hope so!

(ps. I really like the clarity of design docs you're putting out, keep it up! very lucid, makes me feel a bit ashamed at the mess of my note-taking on rust. not to mention total theoretical underpreparedness for what was to come. ah well, hindsight...)

brendanzab commented 6 years ago

I really like the clarity of design docs you're putting out, keep it up! very lucid, makes me feel a bit ashamed at the mess of my note-taking on rust.

Thanks for the feedback! Lots of this is based on the stuff I've learned from being around Rust's development process as its grown over the years, and also through some of the mistakes I've made during the development of my own libraries. The stuff we have learned while working on Rust isn't just all the language/type system features, it's also been all the community and process. That takes time, experimentation, and trial and error to figure out - I couldn't have arrived at this on my own!

That said, there are some definite reactions against some of the early design processes. I'm trying hard to keep my eye on the goal of future formalization and core simplicity of design, as I think that's critical to not becoming a culdesac like C++ has become (and what Rust is trying to dodge becoming with RustBelt). Also in communicating intent in preparation for other contributors coming in to help out. But again, I could have only learned that by hindsight via Rust, and by getting excited about language design and theory thanks to your influence! ❤️