A weird thing?
Conversation
I’m not sure what they are! But yes, maybe predicates. More interested in a graph-based language for nodal editing, but also interested in other projections of the same thing.
1
Some of my colleagues at YesLogic use Mercury, a logic language with explicit ‘modes’. So yeah, that is an inspiration.
2
No clue what the metatheory would look like though. Just very interested in what happens if you start thinking about other ways of looking at functions. 🤔 (I’m probably reinventing _something_) though.
1
Replying to
Oh really? How so? I'm really interested in this - like, I wonder if lambdas are distracting us… but I've got no justification over this. And others may have had this feeling before.
Distractions like variable binding schemes, various optimization passes etc. But perhaps that is unavoidable, no matter what you do? What if moving to something else forces you to pay other costs? Eh.
Replying to
Afaics it’s still CoC (or equivalent), but you could use this interpretation to synthesise proofs maybe.
1
1
Yeah, my intention is pretty much to work in CoC equivalent thingies, but allow for things like modalities and such to be added more gracefully I think? Like, the intention is to ultimately have syntactic room for linearity, phase, uniqueness, etc. for use in systems programming.
1
Show replies
Replying to
Like, so you don’t need to write out a bunch of refl lemmas for every function you write.
1