Conversation

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

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)

Rob Rix‎

@rob_rix

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

Wish I understood levitation at this point - I think it lets you bootstrap datatypes inside the system itself, which feels possibly reminiscent?

You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more

Not seen this one actually! Wondering what bits of a language could be considered 'coeffectful' if anything? Records perhaps?

Still trying to get my head around this mysterious yet tantalizing thingy: ncatlab.org/nlab/show/nece

like, what are records, telescopes, and functions actually doing? 😳 - somehow a record field is 'stronger' than a function parameter - ie. a function can be constructed even if there is no way of providing a parameter, where as a record kind of *insists* that a field is present.

2:07 AM · Apr 3, 2021Twitter Web App

But yeah I might be going off on an unrelated tangent here… 😬

Replying to

and

this comes up because I'm pondering bundled vs unbundled modules - and type parameters vs associated types… but yeah I have no idea what I'm doing so probably should step away from the theory 😟

Replying to

and

I don’t know what bundled vs. unbundled modules are. For type parameters vs. associated types, I guess the latter are existentially bound?