Conversation

Am I misinterpreting your notation or are these predicates rather than functions?

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.

Some of my colleagues at YesLogic use Mercury, a logic language with explicit ‘modes’. So yeah, that is an inspiration.

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.

I think promoting functions to predicates could make certain proof terms more elegant?

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.

Afaics it’s still CoC (or equivalent), but you could use this interpretation to synthesise proofs maybe.

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.

I think predicates could abstract away some decision procedures into handwavey logical unification. I’m not sure if that’s a useful thing for systems programming though?

Replying to