I've implemented dictionary but now the problem is that it's decreasing on another argument. I'm not sure how to re-structure that.

Anyway, it is in the nature of the MiniKanren to ask for certain number of answers upfront so I just limited the depth of recursion.

Y'all think Haskell is so robust with its purity?

Only when you write in something strict you understand how much it is optimized for ergonomics and not for correctness.
Partial functions, unbounded recursion etc break mental model. You can (and should) stay away from them as much as possible and use good subset.

Also Haskell has tons and tons of info these days (relatively ofc). Not at all with Coq which is super old but still lacking a lot of info.

#fp

@charlag The impurity that frustrates me the most in Haskell is asynchronous exceptions. Ugh, such a mess. I suppose partial functions are the most common subset of this problem, in which case we're talking about the same things. But it's funny because even Java is arguably safer around exceptions than Haskell is.

@jamey I don't understand Haskell enough to understand the problem, to be honest. It's not Monad mechanism, it's something else?..

@charlag Yeah, Haskell has this notion of non-monadic exceptions that can be thrown from pure code and, because it isn't monadic, it's really difficult to catch them since you don't know when the exception-throwing code will actually be evaluated. The most common cases are the `error` function in the Prelude (which IIRC is what the compiler generates a call to automatically for partial functions) and things like division by zero, but user-defined exceptions are supported too.

@jamey I see now. I sincerely believe that this type of exceptions if for unrecoverable errors (akin to Error in JVM or crash in Erlang) and should never be used as business logic.

@charlag I agree, and people have tried to retrofit that perspective into Haskell, but I don't think anyone has really succeeded, because, like you said, ergonomics over correctness. Async exceptions are pervasive there because it's easier to call `error` than to either define a safe error-reporting mechanism or to get the type system to prohibit the undesired inputs in the first place.

By contrast, Rust has done a solid job getting correct error-handling to be the more ergonomic choice.

@jamey Rust doesn't have anything Haskell doesn't have I think. Panics in Rust ~ Haskell's exceptions. Different mindset?

@charlag I guess you could say it's about having a different mindset, sure. In terms of the type system, yeah, Haskell has most everything Rust has, and panics aren't that different from exceptions. But for a while there was no way to catch a panic, by design, so people _had_ to use explicit Result types, and lots of library functions and some syntax evolved around that to make doing so ergonomic. (Especially the '?' operator.) So in Rust it's not idiomatic to panic, if there's any alternative.

@jamey I see your point but help me here
? is used to exist from current scope with Result::nothing() (or whatever it's called) right?
Why cannot you have the same thing in Haskell with 'do' notation? Maybe is a monad and you can restrict Either to be it as well

@charlag Yes, that's true; `Either err` is a quite handy monad and its bind operator is roughly equivalent to Rust's '?' operator. But for example, the Rust operator automatically infers conversion between error representations using their Into trait: small difference, but big ergonomic win.

None of this would be hard to do in Haskell, but since it had async exceptions, people used them instead, even in Prelude. And this stuff is contagious, spreading across libraries until it's everywhere.

@charlag I say all this just because I wanted to agree with your original comment: "Only when you write in something strict you understand how much it is optimized for ergonomics and not for correctness." Rust is not even trying to be a particularly strict language like Coq and it's still managed to do some things in a safer and more pure way than Haskell does, which I think says quite a bit about what people valued when designing Haskell.

@jamey @charlag Also, Haskell's initial design was influenced mostly by the bevy of bespoke pure functional languages people made at the time for research. It's less of an issue to stick exceptions into the core when you're looking at it as a popular feature people implemented because it was convienent and nice for experimenting.

@jamey @charlag I’ve been working on `chain`, as an experiment to “improve” error handling in Haskell

https://github.com/lthms/chain — “Extensible, Type Safe Error Handling in Haskell”

But, yay, it does not fix async exceptions.

@lthms Ooh, that's cool! I'm especially pleased to see the "Leverage Existing Error Handling" section since I found those kinds of conversions to be some of the most annoying when I was writing Corrode.

@jamey I really should “finish” it and publish it to Hackage, one day.

@lthms @jamey cool
If I understand correctly, your library does roughly the same thing Eff does?

https://github.com/purescript/documentation/blob/master/guides/Eff.md

I think Haskell is just kinda old, that's why there are design warts (they didn't use monads for IO initially)
Use better Prelude ;)

@charlag @jamey Not really. Purescript, or extensible-effects in Haskell, is about listing the effects of a monadic function, while chain is about listing the error it can encounter.

Chain is more like a type-safe “exception” system, or a more powerful EitherT

@charlag @lthms I agree! There's lots to learn from the many language-design experiments that have gone into Haskell since it was invented in the late 1980s, but in a number of ways it hasn't aged well, so it's good that new languages like Rust get to pick and choose which ideas to adopt.