solomonb

13 ms·

211.
by solomonb 1y ago
yeah i didn't mean to imply you cannot do that, but tactics seem to be highly encouraged. I'm actually a big fan of Lean, I just like it more as a programming language for writing programs with dependent types then as a proof chec
212.
by solomonb 1y ago
This is why I prefer Agda, where everything comes down to pattern matching.
213.
by solomonb 1y ago
Well, I can't speak to your experience but in the case of liftM2 vs liftA2 I have never even seen liftM2 get used. Its more of a historical oddity that it is available.
214.
by solomonb 1y ago
Yes you're absolutely right. I had a bit of a brain fart moment here. If they were Applicative operations then you would not be able to use `liftM2`, not the other way around.
215.
by solomonb 1y ago
Not if you need to perform two /Monadic/ operations as the commenter stated explicitly.
216.
by solomonb 1y ago
I use it the same way but cursor is constantly insisting on making code changes. Is there a trick to get it to introspect on the codebase without wanting to modify it?
217.
by solomonb 1y ago
> When something goes wrong, I don’t hand-patch the generated code. I don’t argue with claude. Instead, I adjust the plan, the prompts, or the agent mix so the next run is correct by construction. I don't think "correct by cons
218.
by solomonb 1y ago
Right on, I'll take a look at your haskell code this week.
219.
by solomonb 1y ago
I'm having trouble reading zig code, so I'm not sure how much overlap there is but I have done some work with mealy and moore encoded as co-algebras in haskell: https://blog.cofree.coffee/2025-03-05-chat-bots-revis
220.
by solomonb 1y ago
What are the pros and cons of Dark Lang vs Unison?
221.
by solomonb 1y ago
In the contemporary art market the stated prices are actually really low. Painters fresh out of art school at a good gallery focused on emerging artists will sell paintings for 10-20k these days.
222.
by solomonb 1y ago
A state machine, or more specifically a Moore Machine.
223.
by solomonb 1y ago
I'm starting a Low Power FM radio station for my local area.
224.
by solomonb 1y ago
Its neat but isn't it basically just `wall`?
225.
by solomonb 1y ago
> One of the fascinating things about lean manufacturing is that few companies outside of Toyota (let alone manufacturing) have ever successfully gone lean. Projects like NUMMI were a failure. Is that really true? I'm asking not deb
226.
What got lost in translation from Lean Manufacturing into Agile?
3 points by solomonb 1y ago|4 comments
227.
by solomonb 2y ago
He can't run again.
228.
Chat Bots Revisited(blog.cofree.coffee)
2 points by solomonb 2y ago|0 comments
229.
by solomonb 2y ago
> I used my mom's typewriter, which she typed her thesis on in the 1950s The point was that later typewriters had a features like memory, automatic indentation and erasing that were not available in 1950s era typewriters..
230.
by solomonb 2y ago
Yeah I understand that the existence of the commutative diagram implies that it typechecks. I was trying to give OP a basic intuition for them. I should have said something like: If you follow the two paths around the square you will find t
231.
by solomonb 2y ago
Its a way of demonstrating that two paths through a diagram are in some sense equal. The dots in the corners are objects and the arrows are morphisms. To keep this simple just imagine the objects are types and the arrows are functions betwe
232.
by solomonb 2y ago
Hi shae!
233.
by solomonb 2y ago
You can desugar let bindings that way but often times (as I believe is the case in GHC) you have a `Let` term in your AST.
234.
by solomonb 2y ago
In a production application you generally don't write code like that. I find it tends to be the opposite problem where you often see giant `do` blocks performing all sorts of monadic effects.
235.
by solomonb 2y ago
mySubroutine = do foo <- mkFoo bar <- mkbar foo mkBaz bar mySubroutineV2 = mkFoo >>= \foo -> mkBar foo >>= \bar -> mkBaz bar
236.
by solomonb 2y ago
You still don't need monads for any of this. Monads give you an ad-hoc polymorphic way of doing monadic actions. Short circuiting on `Either` is a specific case of this. You can define your own EitherBind in any language. eitherB
237.
by solomonb 2y ago
> How can you do "Errors as values" at a large scale without do-notation / monads? You don't need monads for this. You just need the ability to encode your error in some term like `Either e a` and ability to eliminate
238.
by solomonb 2y ago
Words can have many uses. https://en.wikipedia.org/wiki/Optic_(disambiguation) > In computer science, optics are a general class of bidirectional transformations
239.
by solomonb 2y ago
One of my first big personal programming projects was implementing this and a bunch of variations in python many years ago: https://github.com/solomon-b/greedypacker Its still my most starred repo. :shrug:
240.
by solomonb 2y ago
Well for theorem proving you need Sigma and Pi types plus some notion of equality. Can you achieve those with Scott or Church encoding?

More ›