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
Replying to
@brendanzab
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
Show replies