"Did you ever get around to looking at linear type systems?"
I was (and still am) waiting for you to teach them to me :p
My recent explorations are hardening my bias for operational/ugly/imperative approaches over declarative/elegant/functional ones. The trouble with being elegant is that the implementation is harder to tinker with without causing subtle issues. Later readers have to understand global properties at a deep level.
Don't get me wrong, there's room for high-level languages in my world-view. They're just harder to communicate the big picture of, and I want to start with simpler problems. High-level languages and type systems are hard crystals, and I'm currently more interested in building squishy cells.
"I'm currently more interested in building squishy cells."
I respect that, but just to get it written down, here's what I've come up with so far:
All lambda expressions must be lambda-lifted so they're at the top level of some module. (I guess this might count as a lambda-free logical framework.)
Every function type (X -> Y) is annotated as (X -> [C] Y) with the implementation code C of that function's source module. A simple export/import of an X-to-Y function will actually bind an import variable of the type (existscode C. (SatisfiesSignature S C * (X -> [C] Y))), where S is the import signature.
If a module has access to installed implementation code C and it knows SatisfiesSignature S C and SatisfiesSignature S C', then it can conclude C = C'. It can take advantage of this knowledge to get access to fuller knowledge about how an (X -> [C'] Y) function behaves.
---
"I was (and still am) waiting for you to teach them to me :p"
Really? I don't remember where we left off, but let's get in touch on this.
