Uniqueness types for IO

·

4 min read

( Please excuse the odd syntax. Hashnode doesn't support coloring for OCaml. )

Pure functional programming is neat. It allows for some extremely unique optimisations and speed improvements - but it makes usual programming things like IO hard.

Therefore, it makes sense to separate the "doing IO" parts of your program from the "doing computation" parts, so we can optimise the "doing computation" parts as much as possible without affecting IO. One method of doing this is uniqueness types.

Uniqueness types are a way of describing a value that must be unique at every point in a program. For example:

-- In this article I will be using the <type>* syntax for unique types.
-- Note that application binds tighter then uniqueness, so () io* means (() io)*, and not () (io*)

-- x is a unique int
let x : Int* = 10

-- This is invalid: we can't copy a unique value.
let y : Int* = x

-- This is invalid: we can't erase the uniqueness of something.
let z : Int = y

-- This is valid! We can pass unique arguments to functions - we just lose control of the unique argument as soon as we do. This means if we want to get control back, we'll have to return the unique argument back again.
let some_function arg : Int* -> Int* = arg
let k = some_function x

Now, how is this applicable to IO? It's fairly simple - we pass the main function some sort of unique object to be used for IO, and you cannot duplicate it or copy it into some global variable, so you must pass it to every function that wants to do IO.

Let's have a look at a simple implementation.

-- io carries a value to allow for functions that return a value.
type 'a io = unique IO of {...private fields...} * 'a


-- Note that we don't need the <type>* syntax, as the constructor for io is already unique.
let get_value_from_io io_obj : ∀a, a io -> (() io, a) =
    -- neither of these values are unique - but because the constructor is unique and all relevent functions take an `io`, you have to put it back into a unique object for it to be useful.
    let IO (priv, val) = io_obj in
    ( IO(priv, ()), val )


let want_to_do_io io_obj : () io -> (() io, string) =
    let io_obj2 : () io = 
        print_string io_obj "Give me some text> " 
    in
    let io_obj3 : string io = get_line io_obj in
    io_obj3

let main io_obj : () io -> () =
    -- Note how we have to manually pass forwards and back the io object.
    -- Without manually passing it back, we wouldn't be able to do any io after passing our ownly io object to a function.
    let (io_obj2, string) = 
        get_value_from_io (want_to_do_io io_obj)
    in
    let io_obj3 = print_string io_obj2 string
    io_obj3

Something interesting to note is that every function that takes an io must also return one. The reason for this should be fairly obvious - if we pass an io to something, our original io is now invalid, and if one isn't returned from the function, we can't do io ever again.

One thing astute readers might notice is that this takes a lot of time and a lot of writing to do. An easy solution might be to introduce some syntax sugar, like so:

let main io_obj : () io -> () io =
    let (io, concat) = 
        bind io_obj using get_value_from_io in
            let+ string1 = want_to_do_io io_obj in
            let+ string2 = want_to_do_io io_obj in
            (io_obj, string1 ^ string2)
        end
    in
    print_endline io concat

This could then desugar to:

let main io_obj : () io -> () io =
    let (io, concat) = 
        let (io_obj, string1) = 
            get_value_from_io @@ want_to_do_io io_obj 
        in
        let (io_obj, string2) = 
            get_value_from_io @@ want_to_do_io io_obj 
        in
        (io_obj, string1 ^ string2)
    in
    print_endline io concat

This allows for the analysis of purity (anything that doesn't take an io is IO pure ), and is much simpler, in my mind, then something like Haskell's monads. The Clean programming language is the main programming language that currently implements this, and I plan for it to be the method for doing IO in my language, Khasm.