18 June 2012

Strong functional programming


loop :: Int -> Int
loop n = 1 + loop n


loop 0 = 1 + loop 0

0 = 1




Life without ⊥ (bottom)


Not having to deal with ⊥ has a lot of advantages:

Simpler proofs


if P(0)
then for all n, P(n)


Simpler language design

Arguments evaluation


-- a function returning the first argument
first a b = a

-- with strict evaluation
first 1 ⊥ = ⊥

-- with lazy evaluation
first 1 ⊥ = 1
Pattern matching


first (a, b) = a


(⊥a, ⊥b) = ⊥
& operator


True  & True  = True
True  & False = False
False & True  = False
False & False = False

If you introduce ⊥ you have to define:

⊥ & y = ?
x & ⊥ = ?


⊥ & y = ⊥
x & ⊥ = False if x = False
x & ⊥ = ⊥ otherwise


More flexibility in language implementation




    if booleanExpression then expression1 else expression2


    a = true
    if a then b else c => c






Not all green


Not Turing complete



evil :: Nat -> Nat
evil code = 1 + eval code code


-- by definition of the eval interpreter
eval 666 666 = evil 666

-- but if we go back to the definition of evil
evil 666 = 1 + (eval 666 666)

evil 666 = 1 + evil 666



Non terminating!



The rules for non-termination


data Bool    = True | False
data Nat     = Zero | Suc Nat
data List a  = Nil  | Cons a (List a)

and some functions on those types:

-- size of a Tree
size a :: Tree a -> Nat
size Nilt = 0

-- filter a List with a function
filter f Nil = Nil
                       otherwise = filter f rest

Rule n.1: all case analysis must be complete



-- taking the first element of a list
head a :: List a a -> a
head Nil default           = default
head (Cons a rest) default = a


data NonEmptyList a = NCons a (NonEmptyList a)

-- taking the first element of a non-empty list
head a :: NonEmptyList a -> a
head (NCons a rest) = a



Rule n.2: type recursion must be covariant


  1. You can define data types recursively
  2. You can use functions as values
  3. So you can build the following data type

    data Silly a = Very (Silly -> a)

With the Silly data type I can recurse indefinitely:

bad a :: Silly a -> a
bad (Very f) = f (Very f)

ouch :: a
ouch = bad (Very bad)


  • is there a "minimal" set of rules?

I have no answer to those questions unfortunately :-(.

Rule n.3: recursion must be structural


factorial :: Nat -> Nat
factorial Zero = 0
factorial (Suc Zero) = 1



ack :: Nat Nat -> Nat
ack 0 n = n + 1

ack (m + 1) 0       = ack m 1






Coding fast exponentiation


pow :: Nat -> Nat ->
pow x n = 1,                   if n == 0


pow :: Nat -> Nat -> Nat
pow x n = 1,                       if n == 0



-- representation of a binary digit
data Bit  = On | Off

-- we assume a built-in bits function
bits :: Nat -> List Bit

pow :: Nat -> Nat -> Nat
pow x n = pow1 x (bits n)

pow1 :: Nat -> List Bit -> Nat
pow1 x n = 1


Codata for "infinite" computations


data Stream a = Cons a (Stream a)



codata Colist a = Conil | a <> Colist a


Cons (1 + 2) rest = Cons 3 rest


Primitive corecursion


function a :: Colist a -> Colist a

Then we can define functions like:

ones :: Colist Nat
ones = 1 <> ones

fibonacci :: Colist Nat
fibonacci = f 0 1





Coinductive proofs



  • their infinite part are the same



-- map a function on a colist
comap f Conil =  Conil








-- infinite lists
data Colist a = a <> Colist a

-- the tail of an infinite list
cotail a :: Colist a -> Colist a
cotail a <> rest = rest

-- don't do this at home
bad = 1 <> (cotail bad)








-- the comonad operations

-- the dual of return or unit for monads
extract :: W a -> a

-- the dual of bind or flatMap for monads

Intuitively you can think of a comonad as:




nats = 0 <> comap (+1) nats

-- a function taking the first 2 elements of a Colist

-- now, let's cobind firstTwo to nats






Unknown said...

You might want a Nil cases for this data type because otherwise it is an infinite stream.

data NonEmptyList a = NCons a (NonEmptyList a)

Eric said...

You're right, there's a problem, but I don't think I can add Nil like that because that would be empty. What I should write is:

data NonEmptyList a = NonEmptyList a (List a)

Unknown said...

Hi, nice post! BTW you should cite the seminal work by Dave Turner on "Elementary Strong Functional Programming" which deals precisely with these issues.

conor said...

Thanks for putting this together. I'd add that total languages can perfectly well be considered Turing complete if they can express, say, a TM-simulation as a coinductive computation, giving it an honest type which shows that you can run the thing for any finite time but without guarantee of halting. Similarly, you can write a self-interpreter with a type that conservatively overestimates the risk of nontermination.

Total programming makes no effective restriction on the programs you can express, documenting risk honestly with appropriate types. Partial programming makes a severe restriction on the promises you can make your type system deliver.

conor said...

Apologies for duplicate comment, now deleted. Back button considered harmful.

Eric said...

@Unknown, I did cite his work in the "Note" in italics at the beginning of the work. David Turner's article is precisely what brought me to write this post.

Eric said...

@conor, interesting thoughts, I like this idea of "honest types" :-) Would you happen to know if anyone pursued ESFP, with a concrete language, at least for teaching? You write that there's no effective restriction on programs which can be express but I'd like to understand what would be the costs in terms of programming convenience.

Mark D. Albin said...

Good points, thanks for sharing.

Sean Seefried said...

I really enjoyed this post Eric. There is much food for thought in Turner's work. Agda is a strongly-normalising programming language that I've had a lot of fun playing with, although I have yet to try using codata with it.

conor said...

I know that Turner and Telford did some work on ESFP after Turner's initial "manifesto" (the progenitor of the JFP paper). I don't know how far they took it or whether there's a "system".

Tarmo Uustalu gave a talk some years back exploring various monadic encapsulations of partiality. The upshot is that risk of nontermination can be packaged like risk of other effects.

Sometimes, Haskell programmers have reacted to the news that they can still write their dangerous programs, but in a monad, with a distaste which betrays a sense that monadic style is disgusting and suited only to doing disgusting imperative things. I have a certain nostalgie de la boue, looking back fondly on my days writing side-effecting programs applicative style in ML. I'd like to work in the same applicative style no matter which effects (partiality, IO, exceptions, nothing at all...) are enabled and track the permissions in the types. The fact that Haskell does not let me do such a thing, does not mean it's impossible, just that it's a reason to wish for better than Haskell. I've been playing around with alternatives, leading to my new toy, Frank ( Frank makes thunking and forcing explicit, but overloads normal applicative syntax for any free monad you like: Frank's type system checks that you only use the side-effects you're entitled to. Like Eff, there's a construct which enables you to make new effects locally available by showing how to handle them.

I recently gave a talk on the topic where I explore what partial programming might look like in a total dialect of Frank. The idea is that you write a general recursive program just as before, but the value that's constructed lives in a free monad, with recursive calls becoming monadic operations. Then you can pick your own semantics.

Eric said...

Thanks for all the links, I have lots to study from there!

rdm said...

I am somewhat dubious about your treatment of the issue illustrated by division, here. I am not convinced you are wrong, but ...

A general problem seems to be that the implementation models some external process, and the model may diverge from an accurate representation. When this happens, further computation ceases to be useful. And, detecting this issue can be useful for resource management purposes. (I feel that this is a restatement of the halting problem in concrete terms.)

If we limit our scope to problems which can be completely resolved at compile time, this of course is a non-issue. And, there's something to be said for restructuring requirements to eliminate such issues.

But some ill-bounded problems (for example: least squares fitting) seem interesting and are sometimes useful at runtime, even though we cannot guarantee statically that the results will always be valid.

Seth Tisue said...

Eric, you have a rare ability to write clearly on difficult topics. Bravo.

Unknown said...

Thanks Eric for an interesting post. I'm only just starting to explore concepts like total functions, codata etc. One thought I've been pondering is why in purely functional languages like Haskell it's not simply just assumed that all functions are total unless they are marked otherwise by the programmer? That would simplify reasoning and optimization of the majority of the program greatly, and in practice I don't think it would be any more unsafe than assuming all functions are partial. A simple totality checker can then be added to infer obvious cases where totality status is incorrect. Idris is one language which has implemented ideas in this direction.