Idris

96 readers

1 users here now

founded 4 years ago

MODERATORS

pangyuehung@lemmy.ml

How are exceptions handled in Idris? (sopuli.xyz)

submitted 1 month ago by Tiuku@sopuli.xyz to c/idris@lemmy.ml

2 comments fedilink hide all child comments

I've been learning good old Haskell, mostly liking it, but one thing I really dislike is the way exceptions are handled.

It's frustrating that any function can throw just about anything, and this isn't reflected in it's type. Too many times my seemingly sound programs have came crashing down at runtime because some dependency decided to throw an exception. I much prefer the Rust way of doing things where errors are communicated by just returning a value describing it, and panics are reserved for serious trouble (out of memory and the like).

So with that in mind, is Idris for me? I assume that all the usual FP stuff is fine, but how are the exceptions handled?

top 2 comments

sorted by: hot top controversial new old

[–] sloppy_diffuser@sh.itjust.works 1 points 4 weeks ago (1 children)

Been forever since I used Haskell, and not used Idris (hi from scaled).

Currently actively developing in TypeScript with the fp library Effect.

It essentially has a tryCatch function to lift exceptions into an Effect (like an Either type). Since TypeScript doesn't expose exceptions in the type system, its the only way to get errors from other libraries into the type system. They come in without types so we wrap them in our own errors types.

[–] Tiuku@sopuli.xyz 1 points 3 weeks ago

Yeah I find myself doing something similar in Haskell too. Catching exceptions only to return them as Left.