Wish I understood levitation at this point - I think it lets you bootstrap datatypes inside the system itself, which feels possibly reminiscent?
Conversation
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
tbh I think it's not just a dependently typed thing - it's kind of common to languages with simpler types systems too. Sometimes I struggle with the associated type vs parameter question In Rust too, for example.
I suppose it’s existentials, really. I was taking the comparison with un/currying a little too literally.