Conversation

Rob Rix‎
@rob_rix
started writing out semantics for my dark hypothesis (that there’s an effect calculus equivalent to lambda calculus but without let or lambdas, where computations are given meaning entirely by effects)
3
32
Rob Rix‎
@rob_rix
it looks like it’s going to be most convenient to express everything structurally rather than nominally. that is, instead of defining an interface for an effect, you just work locally with whatever operations you feel like providing, and so long as they line up with consumers, 👍🏻
2
4
Rob Rix‎
@rob_rix
they’re named, but the names are a contract between sender and receiver only, i.e. local to a given scope, just like a variable name is a contract between the binding site and any reference sites.
1
1
Rob Rix‎
@rob_rix
to be clear, that’s just the formalism I’m designing. Facet itself uses nominally-typed interfaces, and the closest that will approach structural interfaces is if I allow local or inline definitions of them.
2
1
Rob Rix‎
@rob_rix
yeah. the formalism is a sequent calculus, i.e. not a software engineering system :) so I’m much less concerned about that kind of modularity because it doesn’t even acknowledge the existence of modules (or anything outside expressions, in fact!)
1
1
Rob Rix‎
@rob_rix
that said, extending it to integrate modules into the effect language is a pretty major goal, because I want to use that for parameterized modules, cross-compilation targets, metaprogramming, inline tests, and a bunch of other stuff.
1
1
Brendan Zabarauskas
@brendanzab
Yeah I’ve been wondering about this for Pikelet, where I’m hoping to use records as modules. I love the idea of smooshing together structures, but don’t like the idea that I might then run into issues with fields clashing…
1
1
Rob Rix‎
@rob_rix
yeah, if field names are actually named entities, that problem goes away, altho I suppose it raises the question of where those are defined… who namespaces the namespaces themselves? quis namespa… you know what, never mind the mock-latin
1
1
Rob Rix‎
@rob_rix
Replying to
@brendanzab
Similar problem in my formalism: lambdas are scope + readerish effect. But definitions of ops are functions. Where do you tie the knot? (Currently thinking about jumps instead of functions.)
1
Show replies