Everything (the world) is a pure function (or deprecating the IO monad).

[xekoukou]

Mathematics is nothing more than models , abstractions of the world. Mathematics do not have impure functions or side effects.

More importantly , we do not really care about who performs the computation.

Consider the simple physics equations that describe the motion of two balls of specific mass that hit each other with specific velocity. We could compute their movement, speed with those equations, or we could have the balls hit each other and use a sensor that measures their position, speed.

In agda , the addition of two natural numbers is performed by the arithmetic unit of the CPU, instead of the way they are defined.

In both cases, the computation can actually be erroneous. Consider taking your laptop to the International Space Station. Radiation could alter the result of the addition by the CPU.

My point is that we should deprecate the IO monad . Instead we should model the world as a pure function, and let it perform computations. In many cases, we can check that our model is logically consistent.

Consider the case that we have a variable currentUser :

postulate
  currentUser : String

We ask the user her name the first time and then we keep it at the database. In reality , there may be many different users but the fact that we keep the value and never ask it again means that we have a consistent logic.

Of course, we should update our model to take into account that we have multiple users but all abstractions of the world are pure functions.

[jespercockx]

How would you avoid the usual problems with this approach (e.g. being able to duplicate the world or throw it away)? Last time I checked, linear types were not yet available in Agda.

[xekoukou]

@jespercockx We do not need linear types or the world object because we model the environment as a pure function.

Here is an example. In this case, we have n agents that asynchronously interact with a specific server.

The location of the server is known beforehand and we do not lose messages , thus the environment needs to only perform a single type of computation, the permutation of the messages.

open import Data.Nat
open import Data.Unit
open import Data.Vec
open import Data.Product

AgentComputation : Set
AgentComputation = ℕ

postulate
  n : ℕ
  agentComps : Vec AgentComputation (suc n)
  permutate : Vec ℕ (suc n) → Vec ℕ (suc n)

record Server : Set where
  coinductive
  field
    state : ℕ
    compute : ℕ → ℕ × Server

open Server

server : ℕ → Server
state (server s) = s
compute (server s) x = let r = s + x in r , server r

aServer : Server
aServer = server 0

end : ℕ × Server → ⊤
end _ = tt

h : ∀ k → Vec ℕ (suc k) → Server → ℕ × Server
h zero (x ∷ []) server = compute server x
h (suc k) (x ∷ xs) server = h k xs (proj₂ (compute server x))

environment : ⊤
environment = end (h n (permutate agentComps) aServer)

The agents need to define a function

agentCompute : ℕ

and the server is already defined to compute the sum of the inputs.

The functions end h and environment are computed by the environment. In this case, we need to write some haskell code to send the message from the agent to the server.

The permutation happens by the environment itself, it depends on the speed of the agents computers, the type of computations that each agent has chosen to perform etc.

[jespercockx]

Then I don't think I understand your proposal. I agree that it is good practice to keep as much code pure as possible, but in the end doing some IO at the boundaries of the program is inevitable. Are you suggesting to move this boundary outside of Agda and into the Haskell FFI? In that case, I'm strongly against, as this would make it even harder to use IO in Agda and would also lead to code that cannot be used with other backends.

[xekoukou]

Yes, sending msgs should be hidden. The code will only be written once per backend for each type of environment that we want to abstract. And it will actually be minimal.

Noone actually complains that we have a garbage collector and that we hide the algorithm that selects the memory that is to be freed. (except if you have memory constraints)

With IO, we lose the ability to reason about the whole system. Agda is currently a logical framework for a single program for a single computer.

open import Prelude.IO
open import Prelude.Monad
open import Data.Nat
open import Data.Unit
open import Relation.Binary.PropositionalEquality

postulate
  sendN : ℕ → IO ⊤
  receiveN : IO ℕ
  end : ℕ → IO ⊤

agent : IO ⊤
agent = do
          sendN 4

server : IO ⊤
server = do
           x ← receiveN
           end (x + 2)

-------------------------

agent′ : ℕ
agent′ = 4

server′ : ℕ → ℕ
server′ x = x + 2

postulate
  end′ : ℕ → ⊤

sendAndCompute : ℕ → (ℕ → ℕ) → ℕ
sendAndCompute x f =  f x

environment : ⊤
environment = end′ (sendAndCompute agent′ server′)

proof : sendAndCompute agent′ server′ ≡ 6
proof = refl

Can you prove that the server will add 2 to 4 to get 6. That is a property of the whole system.

(Here sendAndCompute end' and environment are compiled to haskell code we provide by hand.)

[gallais]

Can you prove that the server will add 2 to 4 to get 6

You can do this sort of things by using a different set of types to specify your protocol. You can look into session types for instance.

[xekoukou]

From what I know, session types define a certain order with which messages are sent and received and they make sure that both participants have defined the same protocol.

In my opinion, they are not really necessary. We do not need to specify the order at all in types.

I actually doubt that you can prove the above with session types, because the proof requires the knowledge of the functions agent and server.

[fredrikNordvallForsberg]

My point is that we should deprecate the IO monad . Instead we should model the world as a pure function, and let it perform computations.

Could you phrase your proposal more precisely: what do you want to change or add to Agda? Presumably you do not only want to remove the IO monad, because you can of course already avoid using the IO monad in your own code today, if you prefer.

[xekoukou]

I made this issue mostly to bring awareness that there is a better way of describing distributed systems. I do not know the exact changes that might be needed.

1. I am sure that we need to guarantee logical consistency by guaranteeing that functions that are executed in another agent are pure. To mitigate possible attacks, we need to store all inputs that are received by external agents.

1b. That means that we need a database that stores functions , their specific inputs and the output for these inputs. (with features that are necessary to functional languages, see irmin database in ocaml.)

2. Probably, we will also need some support from the backed to generate code for a specific agent.

3. We will also need to provide boilerplate code for common environments : a. When a message can be lost and msgs can be received out of order. b. When execution is ordered. etc.

4. The ideas of the Unison lang might be necessary as well. (What happens when another agent changes a function's content?)

I am looking forward to working on all of the above in the summer (for the ocaml backend).

[jespercockx]

This looks more like a research proposal than a concrete proposal to change Agda. Also note that IO is not something defined in Agda itself but in the standard library, so (a more concrete form of) this proposal should probably go to there instead.

[xekoukou]

None of the remaining details require any research. They are not that difficult to solve. None of the proposed changes have anything to do with the standard library or any library.

In any case, I hope to have created some awareness that the current methods of interaction with the environment are deeply flawed. If not, so be it.

[jespercockx]

I'm sorry, I'm afraid I just do not understand at all what you are talking about. Like @fredrikNordvallForsberg said, if you have a concrete proposal of what should be changed to Agda (or even better, a PR), I would be happy to read more about it.

[UlfNorell]

Perhaps it would help if you gave some more concrete examples. For instance, what would this program look like under your proposal:

open import Prelude
open import System.FilePath
open import System.File

main : IO ⊤
main = do
  src ∷ dst ∷ [] ← getArgs
    where _ → putStrLn "Usage: copy SRC DST"
  contents ← readTextFile (relative src)
  writeTextFile (relative dst) contents

[WolframKahl]

I think that there have been proposals for fine-grained modularisation of the IO monad in Haskell; something like that would certainly be nice in Agda, and hopefully welcome in agda-stdlib.

@xekoukou , I think that Haste ( https://haste-lang.org/ ) has something (different in different versions) about the distributed aspects you are bringing up. Haste relies on compiler support for compiling to different backends and automatically generating the communication --- relying on that compiler support is, in the case of Haste, a problem, since it is a small project that didn't make it into the compiler maintainers' priorities. (So I still have to keep GHC-7.10.3 around...)

[xekoukou]

@UlfNorell

We can not manipulate files directly. All the data we have is pure functions, some with zero arguments, and all are stored in a single database. (All data are immutable.)

The database stores the inputs and the corresponding output.

postulate
  text : String
 values : N -> String

These postulates could for example be stored in the database, or it could be requested by the user and then stored in the database. (The code that requests the data from the user is haskell / ocaml and is not to be seen in agda.)

If the data does not belong to you, it must belong to another agent, thus there must be a protocol to request it.

I will give you tomorrow two examples for the above cases.

@WolframKahl

I will look into it. Now, I need to get some rest.

[andreasabel]

@xekoukou Is your idea related to interaction trees due to Synek, Hancock and Setzer? Here is a paper Anton and Stephan wrote with me where IO is modelled by coinductive trees: http://www.cse.chalmers.se/~abela/publications.html#ooAgda

[xekoukou]

The main reason we need the IO monad is due to our perception of what the World is. We have modeled the world as a mutable variable. When we interact with it, we change its state, thus the order of interaction is important.

Linear types are needed because they stop us from interacting with a previous state of the world that does not exist. anymore. So linear types are a solution to a problem our model of the world has created.

examples :

a. We can view computer computation as a system that mutates the state of memory and registers of a computer. Haskell uses the Storage class to directly change the state of pointers and thus it requires the IO monad. Since haskell is performing computations, we could have used the IO monad to describe all operations of haskell. But we do not, because we want to use an abstract model of computation that has pure functions.

b. Addition in assembly requires the mutation of a few registers. If we only have the primitives that assembly provides, we need to perform those operations in order. But agda considers addition as a pure function.

(modified from here)

# -----------------------------------------------------------------------------
#
# Assemble and Link:
#     gcc -no-pie add.s
# -----------------------------------------------------------------------------

        .global main

        .text
main:
        push    %rbx                    # we have to save this since we use it

        mov     $43 , %rax      
        mov     $32 , %rbx
        add     %rax, %rbx            

print:
        # We need to call printf, but we are using eax, ebx, and ecx.  printf
        # may destroy eax and ecx so we will save these before the call and
        # restore them afterwards.

        push    %rax                    # caller-save register
        push    %rcx                    # caller-save register

        mov     $format, %rdi           # set 1st parameter (format)
        mov     %rbx, %rsi              # set 2nd parameter (current_number)
        xor     %rbx, %rbx              # because printf is varargs

        # Stack is already aligned because we pushed three 8 byte registers
        call    printf                  # printf(format, current_number)

        pop     %rcx                    # restore caller-save register
        pop     %rax                    # restore caller-save register

        pop     %rbx                    # restore rbx before returning
        ret
format:
        .asciz  "%20ld\n"

@UlfNorell

To not use the IO monad, we should not use primitives that mutate the world like readTextFile, writeTextFile

Instead we should view the World as a computer that performs computations and we should model those computations similarly to all other computations in Agda, as pure functions.

What is the meaning of this? :

_+_ : Nat → Nat → Nat
zero  + m = m
suc n + m = suc (n + m)
{-# BUILTIN NATPLUS _+_ #-}

We have assumed a correspondence between our abstract model of addition and the physical system of the arithmetic unit of the cpu. In other words, we let the environment perform a computation and then we assume that it corresponds to our abstract model.

Let us instead use a postulate here for our next example :

postulate
  _+_ : Nat → Nat → Nat
{-# BUILTIN NATPLUS _+_ #-}

Here, logical consistency requires that the arithmetic unit returns the same result for the same input and that it terminates at a finite time. if 3 + 4 = 5, then this is logical consistent if we get the same result all the time.

If we now take our computer to the International space Station, the arithmetic unit will be an impure function, at one time the result will be 5, another time it will be 8. Assuming that all other operations are working correctly, we could store the first result, and reuse that result every time we are asked to compute 3 + 4.

In other words, we can model a physical system as pure function and maintain consistency even if the physical system is inconsistent.

Our model of the world might be inaccurate but the computation respects our theorems , proofs. All we need to do to make it more accurate is to update our model to take into account parameters of the environment that were omitted.

So, to summarize : The world is not a mutable variable, it is a pure function.

[jespercockx]

To not use the IO monad, we should not use primitives that mutate the world like readTextFile, writeTextFile

As @UlfNorell said, you can already use Agda without using the IO monad or operations like readTextFile. It is still not clear to me what your proposal would actually add to Agda that would allow you to "manipulate the World as a pure function".

[xekoukou]

@jespercockx Let's leave it at that then.

[UlfNorell]

I have an actual file on my actual file system on my very real computer, and I want to copy it. You can't tell me I shouldn't do that without first convincing operating system developers to completely change the way we interact with computers. Good luck with that.

[xekoukou]

@UlfNorell Did you convince Intel to change the assembly language to not have the mov command?

You didn't. What you did was create the correct abstractions that consider addition a pure function instead of mutation of the registers.

As I said before, we need to have a database of immutable data, that is append only.

I wish you could find errors where errors exist.

[gallais]

Having a distributed evaluation model with seamless transmission of data between the various units doing the computation seems orthogonal to IO so why focus on deprecating the IO monad which would, according to you, still be needed to e.g. read a file?

[xekoukou]

By the way, we can interact with the file too, if we want to. Let's use a similar example.

We have a sensor that measures the temperature. It is a mutable variable. How would we represent it as a pure function?

It depends on what information we need.

module temp where

open import Data.Nat
open import Data.Fin

Temp : Set
Temp = ℕ

postulate
  constTemp : Temp

postulate
  varTemp : ∀ k → (Fin k → Temp) → (Fin (suc k) → Temp)

postulate
  Time : Set
  Date : Set

postulate
  tempOfSpecificRoom : Time → Date → Temp

If we need only one value, we use constTemp. If we need all previous values, we use varTemp If we know that there is a way to determine the temperature of a specific room by the date and time, then we use tempOfSpecificRoom

Keep in mind that we assume that this is a pure function, thus if we dont know the specific temperature for a specific date and time, we measure it with the sensor. Then every time we are at the same time and date, we don't use the sensor, we retrieve the value from the database.

@gallais

A. Because of the above, we do not need IO to read a file. B. We can model an environment where we lose data.

Keep in mind that Temporal Logic Of Actions or TLA by Leslie Lamport does not differentiate between the environment and the actions taken by computers.

[UlfNorell]

I still can't see what it is you are arguing here. Under your proposal,

Can I write an Agda program that can be compiled and run to copy a file on my file system?

If yes, can you sketch what it would look like? If no, what are you actually suggesting? That Agda programs should not be able to influence the outside world?

[xekoukou]

Instead of looking at the file, we should model all the programs that can change the file, whether they do it asynchronously or sequentially etc. Thus we model the processes or pure functions and not the variables.

Here is an example, where we model a room that has a radiator , a sensor that measures the temperature and a switch that turns on or off the radiator.

module temp where

open import Data.Nat
open import Relation.Nullary
open import Data.Nat.Properties
open import Data.Bool hiding (_<?_)

Temp : Set
Temp = ℕ

postulate
  Time : Set
  initialTime : Time
  timeAfterAnHour : Time → Time

data RadiatorSwitch : Set where
  on off : RadiatorSwitch

postulate
  user : Temp → RadiatorSwitch

tempRegulator : Temp → RadiatorSwitch
tempRegulator n with n <? 25
... | yes p = on
... | no ¬p = off

postulate
  tempOfSpecificRoomAfterAnHour : Time → RadiatorSwitch → Temp

record Stream : Set where
  coinductive
  field
    val : Temp
    next : Stream

open Stream

system : Temp → Time → (Temp → RadiatorSwitch) → Stream
val (system temp time rad)  = temp
next (system temp time rad) = system (tempOfSpecificRoomAfterAnHour time (rad temp)) (timeAfterAnHour time) rad

-- A system where the user is the regulator and initial time

userSystem : Stream
userSystem = system 0 initialTime user

-- An automated system

automatedSystem : Stream
automatedSystem = system 0 initialTime tempRegulator

(after 24 hours we close the program to simplify the example.)

The tempOfSpecificRoomAfterAnHour function waits for an hour and then measures the temperature of the room with the sensor.

For the automated system :

The tempRegulator opens or closes the switch.

For the user system , we model the behavior of the user with the user function.

It is important to notice that the function tempOfSpecificRoomAfterAnHour has the exact same functionality as the builtin _+_ function we have in agda. It actually performs a computation. And if the room is perfectly insulated, then it is actually a pure function, we have equations that deterministically tells us the temperature after an hour.

In other words, the environment can be seen as a computer.

The are theoretical and scientific questions with regards to the last statement. My point of view is rather practical.

edit :

In fact I think that tempOfSpecificRoomAfterAnHour should change the state of the switch in the same way that addition uses the mov command to move the numbers into the registers.

[nad]

I haven't read the discussion carefully, but I wonder if what @xekoukou has in mind is related to functional reactive programming (FRP).

[UlfNorell]

I take your dodging the question as saying that you don't think that Agda programs should be able to change files on people's computers. I have little sympathy for this view.

[xekoukou]

@UlfNorell They could, but indeed I do not find this feature useful. (I actually thought that my example would suffice.)

@nad I tried FRP before, I found that it was limiting, but I can't remember what it was.

The funny thing is , that people here actually proposed to me to do things that I have actually tried before and they didn't work. So it's like you knew what I was working on, the last years. (Except for TLA, which you didn't figure out.)

Let us take a break from this for a while please. I actually do not know everything there is about it, or how to model the environment. It takes time.

[UlfNorell]

They could, but indeed I do not find this feature useful.

As other people have said, if you don't want to write programs manipulating files you don't have to. But the reality is that file systems exist and there needs to be programs working with them. Arguing that these programs shouldn't be written in Agda because in your view "the world is a pure function" is not helpful.

[bbarker]

This may be getting a bit far afield, however an alternative might be effect types. To bring up the Unison language again, it basically has an algebraic effect system, and was based on the Frank language by Conor McBride, Sam Lindley, and Craig McLaughlin.

I'm far away from being experience enough in Agda or Unison to know what this would look like, but I suppose there's a chance it (or some variant thereof) could be implemented as a library.

One of the big appeals, other than improved granularity of effects, seems to be not having to deal with monad transformers.

[xekoukou]

(To all, )

Agda is a theorem prover and a programming language. That means that we can prove properties of programs, compile them and execute them at the same time.

This is not true for a distributed system where multiple programs need to be compiled. We could either

1. create a model of a distributed system that never compiles to an executable or
2. write executable code that does not permit us to reason about systemic properties.

I provided a possible answer to this : Make the model executable. I also pointed that none of the other solutions is able to do both, whatever the other benefits it might have.

[andreasabel]

@xekoukou

Make the model executable.

I think this is what has been done in verification, e.g., Marino Miculan, Marco Paviotti: Synthesis of Distributed Mobile Programs Using Monadic Types in Coq. ITP 2012: 183-200 https://doi.org/10.1007/978-3-642-32347-8_13 .
You have a (slow) functional executable model to prove your program correct, and you swap it for fast imperative code when you generate the binary you want to run.

[xekoukou]

@andreasabel

I'll look into the paper.

Your description of the technical problem seems accurate. We need to compile away the functions that describe the environment with low level code.