i think the combinator based approach to building standard notions of structure is like. *the coolest thing*
it's like, what if we took parser combinators but applied that to making mathematical objects
Conversation
I think this what is kind of pushing for? twitter.com/jjcarett2/stat For example: arxiv.org/abs/1812.08079
Quote Tweet
Replying to @brendanzab and @PTOOP
type classes (and module types and traits) are all variants of interfaces along with extra rules for conformance and/or resolution. The first step is to revisit interfaces and how to build & compose them. In fact, interfaces should be first class, but they aren't (yet).
1
4
(sorry if you are already aware of this stuff, heh)
1
1
This is indeed an avenue that I've been exploring. I guess I'm "pushing for" it because the difference in what you have to say, as a human, is so much briefer for the same final content, it seems weird to want to say the long thing. But then Java, so meh.
1
2
I think it's cool from a modularity and code evolution standpoint (more thinking of programming than theorem proving here). Would be cool if programming languages let us split up and combine modules after the fact, and let us make shims in a more flexible way…
1
Note: I totally disagree about splitting up after the fact. The meta-theory of that is seriously weird, in not-good ways.
1
1
Oh right! Is this part of why you prefer the ‘tiny theories’ approach?
I guess I'm thinking about how people find ways to split existing structures into smaller ones, but I haven't really though precisely about the issues around it like you have.
That is part of why I prefer 'tiny theories', yes. There are theories which are finitely axiomatizable where if you remove something, the result is no longer finitely axiomatizable! [I don't have good examples, I would have to re-dig in the CASL docs to find.]
1
1
Now I'm curious how this stuff squares with use cases in programming. Do you know if approaches like tiny theories conflict at all with stuff like abstract datatypes?
1
Show replies