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.)
Conversation
Wish I understood levitation at this point - I think it lets you bootstrap datatypes inside the system itself, which feels possibly reminiscent?
3
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?
2
Still trying to get my head around this mysterious yet tantalizing thingy: ncatlab.org/nlab/show/nece
2
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
1
But yeah I might be going off on an unrelated tangent here… 😬
1
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 😟
1
Check out the point starting with "10. Structures are meaninglessly parameterized…" jiggerwit.wordpress.com/2018/09/18/a-r
2
1
Type classes in haskell are usually 'unbundled', where as modules in ML are usually 'bundled'