3 ms·

The "getting bigger" actually happens in reverse. `main` has god-mode privileges, and it can selectively grant smaller or equivalent privileges to the functions

The "getting bigger" actually happens in reverse. `main` has god-mode privileges, and it can selectively grant smaller or equivalent privileges to the functions it calls, which in turn, grant smaller or equivalent privileges to the functions they call. A function can't call another with greater privilege than it has itself. Ideally we should aim to grant only the necessary privileges to functions that need them, with the leaf functions in the call graph being pure functions - those which have no privilege to do anything but compute (or never return, which can be considered a side-effect). We might also want total pure functions, which are guaranteed to return (they only use primitive recursion), though there's no guarantee that they'll return in any reasonable time. Haskell is a pretty lousy example because it bundles everything up into one big `IO` privilege, which gets passed around everywhere, and monads aren't that great. Monad transformers are terrible at scaling.

chuckadams 2y ago
> monads aren't that great. Monad transformers are terrible at scaling. I've dabbled in Haskell, but making anything more than toys became infuriating when dealing with deep stacks of monad transformers: the inscrutable error messages that maybe you just need another `lift` to fix or maybe need to rearrange the whole stack IDK WTF FML LOL. I'm now poking around Unison, though without any ideas so far on what to write with it. The Abilities system looks refreshingly simple, and there's even a fair explanation somewhere on the site of how they're at least as powerful as Monads.
- sparkie 2y ago
  I personally think these effect systems are trying to solve the wrong problem. What we really want is capabilities[1], and the means of enforcing them, which I suspect is best done with linear types and uniqueness types. Granule[2] is certainly of interest as it combines these two typing disciplines. Austral[3] is another worth looking into, though uniqueness and referential transparency is not one of its goals, it does provide capabilities which are encapsulated in linear types, which serve a similar purpose as uniqueness types for guaranteeing unforgeability. [1]:https://en.wikipedia.org/wiki/Capability-based_security https://en.wikipedia.org/wiki/Capability-based_security [2]:https://granule-project.github.io/ https://granule-project.github.io/ [3]:https://austral-lang.org/ https://austral-lang.org/

chuckadams 2y ago

> monads aren't that great. Monad transformers are terrible at scaling. I've dabbled in Haskell, but making anything more than toys became infuriating when dealing with deep stacks of monad transformers: the inscrutable error messages that maybe you just need another `lift` to fix or maybe need to rearrange the whole stack IDK WTF FML LOL. I'm now poking around Unison, though without any ideas so far on what to write with it. The Abilities system looks refreshingly simple, and there's even a fair explanation somewhere on the site of how they're at least as powerful as Monads.

sparkie 2y ago
I personally think these effect systems are trying to solve the wrong problem. What we really want is capabilities[1], and the means of enforcing them, which I suspect is best done with linear types and uniqueness types. Granule[2] is certainly of interest as it combines these two typing disciplines. Austral[3] is another worth looking into, though uniqueness and referential transparency is not one of its goals, it does provide capabilities which are encapsulated in linear types, which serve a similar purpose as uniqueness types for guaranteeing unforgeability. [1]:https://en.wikipedia.org/wiki/Capability-based_security https://en.wikipedia.org/wiki/Capability-based_security [2]:https://granule-project.github.io/ https://granule-project.github.io/ [3]:https://austral-lang.org/ https://austral-lang.org/