Moon and run time errors.

[Kesanov]

I think it would be wise to allow only IO functions to throw run time errors.

What is your opinion?

[VictorTaelin]

Please, be more specific! What do you mean by IO functions? What runtime errors?

[Kesanov]

E.G. should (get [1, 2] 10) throw an error or return Nothing : Maybe a instead?

Should we provide an error functions can throw error from pure code (code that does not communicate with outside world)?

[VictorTaelin]

Oh, I see. So, yes, one of those two things should happen. We should either throw an error to the host language, or change get to return Maybe a instead. What is your vote?

[VictorTaelin]

My argument for not returning Maybe is that get, once typed, would require a compile-time proof key is on the map you're accessing. Something like:

get : ∀ a . (key : String) -> Map (key :: keys) a -> a

So it is still total.

[Kesanov]

Compile time safety would be definitely nice, but won't it make the core language too unreadable? Since Map can return different types the final signature will look like:

get : (key : String) -> (key -> value) -> Map (key :: keys) value -> value

Isn't it too much?

[VictorTaelin]

If it could return different values then that info would be encoded on the Map parameter,

get : (key : String) -> Map ((key, val) :: keys) -> val

Right? Point is, we'd push the complexity to the type level. At value level nothing would change.