there are a set of features in functional programming that people would expect in dependently-typed functional languages and they're not (fully) available yet.
Conversation
This Tweet was deleted by the Tweet author. Learn more
extensible records, effects, interfaces. also minor stuff like modules, namespaces, etc. the main question in my head at all times is "how can I make this ergonomic without breaking the theory?"
2
7
Ohhh yes I want all of these things so bad
1
1
specially modules and namespaces that seem so trivial but they super matter if you don't want your future package manager to suck tremendously.
2
5
Yes I want nice modules so bad. Namespaces are also interesting but I don't understand them as much. Also interested in how stuff like staged computation interacts with package managers. Like it would be cool to be able to avoid depending on packages that have been inlined away.
1
2
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
same boat here :( my best idea so far is to treat them like (non-extensible) records.
1
1
The fact that they’re extensible records seems (almost) the whole point, otherwise you can just use Coq modules. “Open” namespaces _can_ be encoded in Coq, exploiting its lookup rules — much more easily than anything in math-comp, and I do it by hand, but it’s still annoying.
2
Yeah, not sure I understand the 'not being extensible thing'. I'm sort of thinking of namespaces like in Lean, C++, etc. Like you can split namespaces over multiple files and build them up incrementally. But we might be talking about different things?
2
1
One thing I want to figure out is a nice way to scope data constructors under the name of a type, like in Rust and Lean. Would be cool to have some sort of systematic approach to extending 'paths' like this, but I dunno what that would look like…
Like, I kind of think of the 'path' as like a 'bookmark' that makes it easy for the programmer to find stuff in a sort of soup of nodes… like, it's more of a user interface thing? I dunno though
1
But if it's only a user interface thing, then it's less… uhhh… 'first class'. Which could be good, but I dunno.
1
Show replies