Learn You an Agda

Agda-mode will translate from symbol names to unicode for you. For example, \\to gets translated to → and \\== goes to ≡. It is very easy to work with after a short learning curve. There is more explanation available on the Agda Wiki. [0]

[0] http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.Unicod...

> Languages that use types for elaborate proofs always seem to me like they only prove the most uninteresting properties of programs, namely the parts that deal with data transformations.

> At the end of the day, programs are written for their side effects

The reason for such a focus on data transformation is that it's very easy to do in these purely functional languages (Agda included). It's so easy, in fact, that "other" things, like side effects, event handling, etc. are represented as data transformations. This is most obvious in Haskell, since laziness decouples definition from computation; eg. making it trivial to represent event streams as infinite lists.

> What I'm most interested in is proofs that, say, in a concurrent environment, a function that closes a socket will never be called as long as there are pending tasks to write to the socket.

The usual approach is to define a datatype of operations you might want to perform (eg. `Write String`, `Read Length`, etc.). Next you define a datatype which can combine these operations together in ways you may want (eg. something like a rose tree, if you want threads firing off threads). This forms an "embedded domain-specific language". We then write a bunch of helper functions for manipulating these datastructures (eg. a "combinator library"), then we use these to write down what we actually want as a combination of operations.

Next we write an interpreter function which opens a socket, performs all of the operations in the tree (possibly in multiple threads), waits for them to finish then closes the socket.

> Or, because I write concurrent data structures, I'm interested to prove that a certain function will eventually release all locks it acquires. Are there any such languages?

You can do the same thing as with the socket example, except you can strengthen the type of your program (operation-combining) datastructure to enforce that locks are released. As a simplified example, we can force a serial computation to release locks by only allowing AQUIRE and RELEASE to be inserted together:

    data Op = Foo | Bar | Aquire ID | Release ID

    data SafeOp = SFoo | SBar

    data Program : Type where
      NoOp : Program  -- Empty Program
      WithLock : Program -> Program  -- Add lock ops to a Program
      PrefixOp : SafeOp -> Program -> Program  -- Add a non-lock Op to a Program
      Interleave : Program -> Program -> Program  -- Combine two Programs

    -- Part of the interpreter, not exposed to the world
    progToOps : Program -> [Op]
    progToOps NoOp = []
    progToOps (WithLock id p) = [Aquire id] ++ progToOps p ++ [Release id]
    progToOps (PrefixOp SFoo p) = [Foo] ++ progToOps p
    progToOps (PrefixOp SBar p) = [Bar] ++ progToOps p
    progToOps (Interleave p1 p2) = interleave (progToOps p1) (progToOps p2)

    interleave [] ys = ys
    interleave (x:xs) ys = [x] ++ interleave ys xs

Notice that progToOps can never output a list containing Aquire without also containing a Release with the same ID. Also notice that we can define arbitrary combinations of the other ops:

    [] is NoOp
    [Foo, Bar] is PrefixOp SFoo (PrefixOp SBar NoOp)
    [Foo, Aquire A, Bar, Aquire B, Release A, Foo, Release B] is Interleave (PrefixOp SFoo (PrefixOp SBar NoOp)) (Interleave (WithLock A NoOp) (WithLock B (PrefixOp SFoo NoOp)))

Of course these datastructures would be build up by helper functions instead of by hand, would be tree-like for concurrency, would probably provide guarantees per sub-tree, would allow arbitrary functions (of some suitable type) in place of Foo, Bar, etc.

Note that `false` the value of type `Bool` is not defined in terms of bottom. It is a constant in its own right just like `nil` and `cons 1 nil` are.

What happens in Data.Bool is that we have the function from values to types `T` such that `T true` and `T false` are types equal to top and bottom respectively. This value-to-type encoding is called a "universe" and allows us to talk about propositions which are based on boolean function results like

    theorem1 : T (1 - 1 == 0)

which is somewhat interestingly different from

    theorem2 : 1 - 1 = 0

in that the first will reflect upon the definitions of the (recursive) functions (-) and (==) while the second reflects only upon the definition of (-).

Not guilty! I picked this one up on Twitter this afternoon, but it's possible the lineage traces back to your lobste.rs post. (I have no lobste.rs account, though not for lack of interest -- while sparse, the comments there seem to be of very high quality.)

But in your example the program doesn't represent the code itself but a program written in some new language. I said that current type systems are good for writing compilers, but not so good at describing their own behavior other than data transformations.