Arc Forumnew | comments | leaders | submitlogin
2 points by akkartik 3522 days ago | link | parent

"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.

2 points by rocketnia 3522 days ago | link

"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.