As such, unprivileged users are permitted to write and execute functions without the possibility that they will be able to access information or resources that are not allowed to access. This is accomplished by enforcing Haskell's strong type system.
Further on, it says:
Trusted functions must return type PGm (Maybe result) where result is the appropriate Haskell type as determined by the return type of function while untrusted functions must return type IO (Maybe result). The PGm monad type can be imported from the PGutils module.
This makes some sense intuitively, but it would be good to see the details worked out. There is always `unsafePerformIO`, after all...
However, I doubt Safe Haskell (without extensions) is formally verified, and it still uses GHC’s runtime, which could have RCEs. Also note that it doesn’t prevent infinite loops or memory exhaustion, the latter even during compilation.
My dream would be a database where Haskell is the query language. It's more expressive than SQL and more composable. Every time I see a new SQL feature that would be trivial in a modern language it feels like we're working harder instead of smarter.
Sooooo if you use a SQL database and a Haskell access library, you kind of get this.
Like esqueleto for instance. With it, you basically use Haskell as a meta-programming language for SQL. It's really nice when it works.
But yeah..makes me think that a more first-class thing would be even better.
Tbh, maybe Haskell compiled to a lower-level query language would be better. A language that is about tables and btrees etc. Where there's no planner because the low-level language is the plan.
As far as query languages go, you may want to look into prql, kusto or google's alternative (i forgot its name). They are composable, and more natural.
> Unlike most database management systems (DBMS), Project:M36 is opinionated software which adheres strictly to the mathematics of the relational algebra. The purpose of this adherence is to prove that software which implements mathematically-sound design principles reaps benefits in the form of code clarity, consistency, performance, and future-proofing.
> Project:M36 can be used as an in-process or remote DBMS.
> Project:M36 is written entirely in the Haskell programming language.
I made something like this for Morgan Stanley some years ago, a structurally typed eager variant of Haskell with static elimination of type class constraints (so no runtime penalty for overloading) and uses LLVM for the back-end:
http://github.com/morgan-stanley/hobbes/
We used it for processing and analyzing billions of events per day. Using structural algebraic types let us encode market data (obviously) but also complex data structures inside trading systems that we could correlate with market data.
As you say, Haskell-ish expressions are much more compact and capable than SQL, which was one of the reasons I wanted to build it.
It also had a somewhat novel compression method (“types as probabilities” if you like the old Curry-Howard view), which was very important to manage billions of daily events.
12 comments
[ 2.5 ms ] story [ 42.9 ms ] threadAs such, unprivileged users are permitted to write and execute functions without the possibility that they will be able to access information or resources that are not allowed to access. This is accomplished by enforcing Haskell's strong type system.
Further on, it says:
Trusted functions must return type PGm (Maybe result) where result is the appropriate Haskell type as determined by the return type of function while untrusted functions must return type IO (Maybe result). The PGm monad type can be imported from the PGutils module.
This makes some sense intuitively, but it would be good to see the details worked out. There is always `unsafePerformIO`, after all...
The answer seems to be Safe Haskell: https://downloads.haskell.org/ghc/latest/docs/users_guide/ex...
(Source: Safe extension mentioned in https://github.com/ed-o-saurus/PLHaskell/blob/d917f0991a455c...)
The PGm monad seems to be an instance of §6.18.1.2. Building secure systems (restricted IO Monads): https://downloads.haskell.org/ghc/latest/docs/users_guide/ex...
> There is always `unsafePerformIO`, after all...
Forbidden in untrusted code by Safe Haskell.
However, I doubt Safe Haskell (without extensions) is formally verified, and it still uses GHC’s runtime, which could have RCEs. Also note that it doesn’t prevent infinite loops or memory exhaustion, the latter even during compilation.
Like esqueleto for instance. With it, you basically use Haskell as a meta-programming language for SQL. It's really nice when it works.
But yeah..makes me think that a more first-class thing would be even better.
Tbh, maybe Haskell compiled to a lower-level query language would be better. A language that is about tables and btrees etc. Where there's no planner because the low-level language is the plan.
> Unlike most database management systems (DBMS), Project:M36 is opinionated software which adheres strictly to the mathematics of the relational algebra. The purpose of this adherence is to prove that software which implements mathematically-sound design principles reaps benefits in the form of code clarity, consistency, performance, and future-proofing.
> Project:M36 can be used as an in-process or remote DBMS.
> Project:M36 is written entirely in the Haskell programming language.
We used it for processing and analyzing billions of events per day. Using structural algebraic types let us encode market data (obviously) but also complex data structures inside trading systems that we could correlate with market data.
As you say, Haskell-ish expressions are much more compact and capable than SQL, which was one of the reasons I wanted to build it.
It also had a somewhat novel compression method (“types as probabilities” if you like the old Curry-Howard view), which was very important to manage billions of daily events.
Good times.
Sieve is O(n log log n) but trial division is O(n^2)