For a sig like:
fillPrimes :: Array Int -> Int -> Int -> Int -> ()
The fact that there is no 'IO' constructor in that type doesn't mean that side effects aren't being tracked. The type inferencer knows what's going on, and so does the optimiser, you just don't have to write effect information in sigs if you don't want to.
If we add all the information about effects and mutability we actually have:
fillPrimes
:: forall %r0 %r1 %r2 %r3 %r4
. Array %r0 (Int %r1) -> Int %r2 -> Int %r3 -> Int %r4 -(!e0)> ()
:- !e0 = !Read %r0 + !Read %r1 + !Write %r1 + !Read %r2 + !Read %r3 + !Read %r4
, Mutable %r1
A term like Array %r0 (Int %r1) means that the fillPrimes accepts an array of boxed integers. The pointers (handles) to those integers are in some region named %r0, and the integers themselves are in region %r1. The effect term !Write %r1 reveals that fillPrimes updates those integers, which requires them to be mutable, hence the Mutable %r1 constraint.
Writing sigs this way is a bit verbose, so we also support the following "short hand" syntax. This sig gets desugared to the previous one using some simple defaulting rules:
fillPrimes :: Array (Int{modify}) -> Int{read} -> Int{read} -> Int{read} -> ()
Full information about effects and mutability is exported in the interface files. I'm currently working on a system whereby you can say "These are the effects I think this function has, but tell me if you think it has more." I'll post more about this when it's done (it half works now).
The problem with inference is, as I understand it, that you're effectively (heh) "impure by default", at least as far as a reader is concerned (if the type isn't explicit you have to assume it's impure, right?). You will get no warning if all of a sudden a function you thought was pure became impure, because some distant thing it depends on was changed to do some IO, or whatever.
ReplyDeleteI understand that in some cases purity will be required (e.g. parallel computations), but sometimes you just want "f x" to be a function invocation unless it's clear from its signature that it's not a function. If that signature hides the effects by default, then that also means it can change without anyone noticing.
I'd prefer if pure was the default and impure, or "either" required an extra annotation.
You're effectively "effect polymorphic" by default, and you can instantiate to either pure or effectful as you wish.
ReplyDeleteIf you specify what effects (or not) a function should have in its signature, and some distant thing causes it to do an IO operation that wasn't in that signature then you'll get a type error.
Whether you prefer to leave your functions effect polymorphic or make them all pure is up to you. Disciple allows both programming styles, but doesn't enforce either one.
"Effect polymorphic" is, in practice from a reader's point of view, impure since you can't assume purity.
ReplyDeleteAnd that's the problem. By default, things can be turned impure by some distant thing changing. Which means that by default you can't assume pure semantics, which is an issue to me. I think purity should be the default, while effects should require an explicit opt-in.
Effect polymorphism is good stuff, but I don't think it should be the default since it allows effects to seep through your whole program without anyone necessarily noticing unless they did extra work to signify that they expected pure semantics. Purity shouldn't require extra work, IMO.
Actually I'd be fine with being generic by default for *inputs*. After all, the caller chooses what to pass in, so if it's effectful it makes sense that the callee is too (e.g. a map function). It's just when the effects *originate* from the function body itself (rather than from inputs) that I think you should have to explicitly opt-in, so that you can't accidentally become effectful by one of the libraries you call being changed.
ReplyDelete"Effect polymorphic" is, in practice from a reader's point of view, impure since you can't assume purity.
ReplyDeleteWhose fault is it if you're assuming purity, but you don't tell the compiler that by providing an effect annotation to enforce that assumption?
I'm not assuming purity, I'm assuming impurity. That's the whole point. In my opinion a modern language shouldn't force me to assume impurity - purity (easy to reason about) should be the default. Not something I have to explicitly specify.
ReplyDeleteIf you call an effect-polymorphic function you therefore have to assume that it's impure, or could become impure at some point in the future without the compiler telling you, which means that in practice it's really impure-by-default with extra work required to specify that you expect something to be pure. The fact that the compiler tracks the effects doesn't help me as a programmer to avoid surprises.