Effect systems are a trend that will go away. You can't statically guarantee that only, for example, the DB has side effects in a function. So what's the point? Haskell got it right in the first instance: IO or pure.
The point of effect systems isn't to stratify the behaviour of the operating system (it's the Wild West out there). It's to stratify the behaviour of your program. A function that has a DB effect isn't telling you that it will make Postgres queries (which can do anything!), it's telling you that it wants to make DB queries so you need to pass it a handler of a certain form to let it do that, hexagonal architecture style.
But you can also stratify in the other direction. ‘Pure’ functions aren't real outside of mathematics: every function can have side effects like allocating memory, possibly not terminating, internal (‘benevolent’) mutation, et cetera. When we talk about ‘pure’ functions we usually mean that they have only a particular set of effects that the language designer considered ‘safe enough’, where ‘enough’ is usually defined with reference to the ergonomic impact of making that effect explicit. Algebraic effects make effects (and importantly effect composition — we got here in the first place because we were fed up of monad transformers) more ergonomic to use, which means you can make more effects explicit without annoying your users.
I'm willing to bet the contrary: that IO-wrapper effect systems are the future of Haskell (particularly Bluefin, but then that's my library, so I would say that).
> You can't statically guarantee that only, for example, the DB has side effects in a function
Most big corporates have their own inner sourced css components library. So when you get design feedback you wouldn't be directly editing the style in one self contained web application, which is what this demo is assuming.
Makes a lot of sense in textbooks. But in the real world, when politics is involved, the whole theory breaks down. What does your text book say about China holding rare earths hostage in regard of comparative advantage?
Someone else starts their own mines, everyone goes a little poorer.
except for oil, most countries aren't dependant on other countries just to survive in the near term (food is one of the few things countries will usually attempt to ensure they are selfsufficent in, if it's feasible)
The UK is far from self sufficient in food. You'd think they would have learned from their mistakes after they nearly starved to death due to the Axis blockade during WWII, but apparently not.
So it seems the thesis of some pretty in the know mathematicians is that the secret of dependent types is knowing when not to use them. Is that necessarily an argument against Lean or Rocq? In the sense could one simply just not use the dependent types on offer in these languages in certain circumstances, and try emulate an Isabelle proof using custom built tactics?
>It has been some time I worked seriously in a dependently-typed language, but I recall coming to the conclusion that dependent types are best used as little as possible, for exactly this reason.
I was referring to issues that arise around the need for heterogeneous equality.
As an example, consider the dependent vector type `Vec n`, which is an array of length `n`. An `append` function would have type `{n m: Nat} -> Vec n -> Vec m -> Vec (n + m)`. That is, it takes an array of length `n`, and array of length `m`, and produces an array of length `n + m`.
Now imagine that you want to show that `append` is associative. That is, for all `x: Vec n`, `y: Vec m`, and `z: Vec o`, you have `append (append x y) z = append x (append y z)`. We can't prove this because we can't even state the theorem; it is not well-typed. The left-hand side has type `Vec ((n + m) + o)`, while the right-hand side has type `Vec (n + (m + o))`. Those two length values are of course propositionally equal, but they are not definitionally equal in type theories like Lean or Rocq's. That is, the equality is not immediately apparent to the type checker, and so requires a proof. But even with a proof, the statement is ill-typed (because equality is "intentional", not "extensional"). So you have to use a heterogeneous equality operator which allows you to compare two values whose types are propositionally but not definitionally equal. This equality is generally more difficult to work with.
Obviously this whole problem goes away if we use a non-dependent array type, as opposed to something length-indexed like this `Vec` type. So unless there is some reason to use the indexed type (e.g., perhaps the compiler can emit more efficient code), I would just use the non-indexed types and prove separately anything I want to know about the length.
React is dead easy to create a component and get going with whatever you want to create. But as your application grows it is really difficult to test. The React testing library sounds good in principle, but once you have useEffects, hooks, the DOM, and every other side effect running interwoven with your component logic, it becomes difficult test. Obscenely difficult. I think there's some tradeoff operating here. I want a front end framework that makes it a little easier to test, happy to go through some more pain to write components.
I preferred class based components. The pretend functional programming style of hooks is quite imperative when you prick a little beneath the surface, so classes were probably the right abstraction.
The problem with classes that hooks helped with was how hard it was to add multiple, reusable bits of lifecycle functionality. In even a medium size codebase I'd find myself having to reason about how to combine behavior A with behavior B in the onComponentWillWhatever methods. Hooks are weird but much much easier to compose and share.
It's not principally about convenience though is it? It's about defining the semantics of your program through the DSL. Then you can verify the program logic, prove properties about it if you wish. It is denotative.
