Conversation

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)

Rob Rix‎

@rob_rix

Apr 3, 2021

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, 👍🏻

Brendan Zabarauskas

@brendanzab

Apr 3, 2021

Will the structural effect operations be labelled?

Rob Rix‎

@rob_rix

Apr 3, 2021

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.

Rob Rix‎

@rob_rix

Apr 3, 2021

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.

Brendan Zabarauskas

@brendanzab

Apr 3, 2021

Nice, seems like this might address this concern

Quote Tweet

Brendan Zabarauskas

@brendanzab

· Apr 3, 2021

Replying to @brendanzab and @rob_rix

Been a bit spooked with the ‘stringy’ nature of the implementations row labels I’ve seen. Seems to pose some issues for modularity? I dunno.

Rob Rix‎

@rob_rix

Apr 3, 2021

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!)

Rob Rix‎

@rob_rix

Apr 3, 2021

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.

Brendan Zabarauskas

@brendanzab

Replying to

@rob_rix

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:22 AM · Apr 3, 2021Twitter for iPhone

Replying to

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

Brendan Zabarauskas

@brendanzab

Apr 3, 2021

Yeah! It gets a bit weird! Clojure lets you have ‘namespaced symbols’ but that requires a top level namespace thingy. Where as I would love to be able to get rid of the top level ‘command’ language (like in Dhall and Nix)

Show replies