Functions allow I/O side-effects without annotation

Bug #892922 reported by Matt Giuca
6
This bug affects 1 person
Affects Status Importance Assigned to Milestone
Mars
Fix Committed
Medium
Matt Giuca

Bug Description

Mars is designed to be a purely declarative programming language, yet there is a gaping hole in that it allows arbitrary IO side-effects such as reading and writing to files. This should be fixed in order to claim that Mars is a pure programming language. It is unclear what the best way forward is, but we do not want to add a lot of complexity to the language (it is fine to special-case IO effects as a language feature without adding a general-purpose monad, uniqueness or effect system).

Also add a built-in __impure_trace :: String -> Void which prints to stderr without requiring an IO annotation. Add a module debug which provides the alias "trace".

Tags: language
Revision history for this message
Matt Giuca (mgiuca) wrote :

Proposals:
1. A simple "io" annotation feature on functions. Functions are required to use the "io" annotation in order to call another io function. For example, "def io <name>".

This has a major problem with higher-order functions. If you are allowed to turn an io function into a first-class function object, does it lose its annotation? If so, only io functions could call function objects (unacceptable). If not, the io annotation needs to be part of the type system. Thus this proposal would lead to a complication in the type system where there is a new function type constructor, "->io". For example, if you turned put_char into a first-class function, its type would be Int ->io Int. As a consequence, it wouldn't be usable in map (which is desirable). As a consequence, it may be necessary to have a way to convert a -> b to a ->io b (or maybe not).

2. A monad, like Haskell. We can special-case IO so there is no need for a monad class. This would mean introducing a new type IO :: * -> *. A function which does IO would be put_char :: Int -> IO(Int). The problem is that we don't want to have to use bind or introduce a new "do" notation (which is incompatible with our existing sequencing) to make it work. We want this code to be valid:

def print_string(str :: Array(Int)) :: IO(Int):
    var i :: Int
    i = 0
    while lt(i, array_length(str)):
        put_char(array_ref(str, i))! # Does IO
        i = add(i, 1)
    return 0

Note the new syntax when calling an IO procedure. We can just use IO as a type-system indicator rather than treating it as a first-class value as Haskell does. Special rule: Calling a function that returns IO requires the use of the ! (it is not possible to, say, assign an IO(Int) to a variable). The ! is not allowed unless the current function's return type is IO. Special rule: An IO type is not convertible to a type variable (so Int -> IO(Int) cannot be cast to a -> b).

I feel this has too many special cases, and monadic IO is best left to lazy languages (which can actually represent IO(a) as a first-class value without executing the IO actions).

3. A World type which must be explicitly threaded in and out of every io function. This is verbose, but that's acceptable. The problem is that it requires uniqueness guarantees. Mars is getting a uniqueness system, but that isn't ready yet and there are no details yet on whether it will be possible to require a unique variable (currently it is just an optimisation).

As troublesome as it sounds, #1 seems to be the simplest. It is effectively the monad approach, but with io as a special keyword rather than a type (and therefore not having to add lots of special cases to the type system).

summary: - Functions allow I/O side-effects
+ Functions allow I/O side-effects without annotation
Revision history for this message
Matt Giuca (mgiuca) wrote :

In progress on branch lp:~mgiuca/mars/io.

Changed in mars:
status: Triaged → In Progress
Revision history for this message
Matt Giuca (mgiuca) wrote :

Test cases required:

- Call global IO function from IO context (should allow) and non-IO context (should reject)
- Partially-apply IO function from IO context (should allow) and non-IO context (should allow) -- result type must be IO
- Lift IO function from non-IO context (should allow)
- Call lifted IO function from IO context (should allow) and non-IO context (should reject)
- Call passed-in IO function from IO context (should allow) and non-IO context (should reject)
- Partially-apply lifted IO function from IO context (should allow) and non-IO context (should allow)
- Use eq/show on IO function type (should succeed)
- Syntax ->io(a, b) as an alias for (a -> io b)
- Somehow manage to unify a non-rigid type variable in the call to a function, then later have it be an IO type (this seems to break at the moment) -- I don't think it is actually possible to expose this case
- CGC that declares itself as IO (should reject)

Revision history for this message
Matt Giuca (mgiuca) wrote :

Fixed in trunk r1293.

Changed in mars:
status: In Progress → Fix Committed
To post a comment you must log in.
This report contains Public information  
Everyone can see this information.

Other bug subscribers

Remote bug watches

Bug watches keep track of this bug in other bug trackers.