C9 Lectures: Dr. Erik Meijer - Functional Programming Fundamentals Chapter 5 of 13 | Going Deep

rgruian

Great post, again. Looking forward to the next one in the series!

exoteric
I : Next<I>

Is time an effect and should type-systems track it?

ShinNoNoir

In reply to exoteric

#Nov 4th @ 2:14 PM

Well, ask yourself this: is time always an effect? For example, does the result of sqrt(9) depend on the current time? Smiley

But when time does have an effect on the result, the type system should track it. For example, getCurrentTime in Haskell has type IO UTCTime.

exoteric
I : Next<I>

In reply to ShinNoNoir

#Nov 5th @ 4:15 AM

If it takes infinite time, then it's a clear effect. If it takes t time, then you could say that the result is t time in the future, rather than t-n time in the future - in a manner of speaking it's living in a different world.

I'm thinking in terms of the environment, time is like state transitions and every state transition is an effect in the world. Of course there's no direct relation between a pure functions definition and how many state transitions it might take to finish, given a multitude of compiler rewritings, hmm...

There is also the matter of dealing with complexity as a tool to know when to parallelize. If a function could be automatically complexity-analyzed then for every function you would know how expensive it was. This would allow you to also express in the type-system a higher-order function accepting another function which must have a complexity lower than a certain bound: the compiler and type-checker would guarantee this to be true. Also you might define functions with time-guarantees, that forcefully stop prematurely if they cannot complete within some time; or never "start" in the first time, given the former example.

For DateTime.Now it is clear that the function is not pure, it takes nothing and returns something different every time - there it is clear that the result is time itself and time never stops changing - it's predictably impure. Erik mentioned modelling time as an IObservable where you can sample it a couple of times; I'm not sure that's really truly pure as the IO, when you subscribe to it, will return different results every time - which is intended of course; but that's kind of hard to get around.

The question is: for infinite time, you have bottom, i.e. non-termination. But how much time is bottom? Is it always sufficient to say infinite time or wouldn't it make sense to define more soft times?

ShinNoNoir

In reply to exoteric

#Nov 5th @ 1:23 PM

"Also you might define functions with time-guarantees, that forcefully stop prematurely if they cannot complete within some time;"

Hmm, that's not an easy task. You'd need to encode values as types or you need type constructors that also accept values instead of only types. For example, you'd love to write code like this then:

-- an Int to Int function that takes at most 5 time units
someComputation :: Int -> RealTime 5 Int

But now you might also want to do arithmetic at the type level:

-- an example, the type of a function that adds two real-time int results:
add :: RealTime t1 Int -> RealTime t2 Int -> RealTime (t1+t2) Int

I think this is getting quite tricky real fast.

(There is a nice way however to pass values around at the type level, see this paper: Functional Pearl: Implicit Configurations —or, Type Classes Reflect the Values of Types)

"The question is: for infinite time, you have bottom, i.e. non-termination. But how much time is bottom? Is it always sufficient to say infinite time or wouldn't it make sense to define more soft times?"

Bottom is the result of anything that fails to produce an answer. I wouldn't overload bottom for computations that do not finish in time, but use the type system instead to tag your values:

-- pseudo-Haskell (no support for values at the type level)
data RealTime <Int> a
 = Result a    -- the result of a successful RealTime computation
 | Aborted     -- the result of a computation that took too long

Edit:

Just found this, might also be an interesting read: Pausable IO actions for better GUI responsiveness.

exoteric
I : Next<I>

In reply to ShinNoNoir

#Nov 5th @ 2:26 PM

Interesting ShinNoNoir. Actually, I've scribbled up a few loose thoughts about this but in the next post I'll maybe write one of the combinators I've been thinking about: namely the computation pre-emption' combinator. So this would spawn a thread (or maybe task) and synchronously wait for that task to complete until some time has passed whereafter it will timeout. This makes timeout or hard limits a pervasive concept in functional programming, if you will. One may say the implementation will be very ugly - depends on OS and .Net primitives - but the abstract idea is quite cool.

There are many aspects to time and computation and this is probably something where someone as Beckman could talk for hours.

I'll look into the pausable IO actions - looks good - but threads provide a brutal alternative: they are not sensitive to the granularity of a task, hopefully the OS will ensure that a thread will be interrupted after some time t.

As for⊥: well the idea is not to misuse bottom but merely to point out that there is a continuum (likely not infinite) between This Instant (!) and Not Ever (⊥). There is space here to be explored, I find that quite fascinating. People talk about the elephant in the room in relation to parallelism; well time is everywhere and it's not mentioned in any type - talk about a taboo topic!'

' This is probably the wrong name, as I now understand pre-emption to actually mean mature or natural completion of a task ahead of schedule, not forced pre-emption but I don't know the precise term to use for this concept

''

exoteric
I : Next<I>

In reply to exoteric

#Nov 5th @ 3:04 PM

The Haskell page for ⊥reveals something interesting!

Bottom is a member of any type, even the trivial type () or the equivalent simple type:

data Unary = Unary

If it were not, the compiler could solve the halting problem and statically determine whether any computation terminated (though note that some languages with dependent type systems, such as Epigram, can statically enforce termination, based on the type for particular programs, such as those using induction).

The important part!

...note that some languages with dependent type systems, such as Epigram, can statically enforce termination, based on the type for particular programs, such as those using induction...

Let's look at Epigram

Epigram is the name of a functional programming language with dependent types and of the IDE usually packaged with it. Epigram's type system is strong enough to express program specifications. The goal is to support a smooth transition from ordinary programming to integrated programs and proofs whose correctness can be checked and certified by the compiler. Epigram exploits the propositions as types principle, and is based on intuitionistic type theory. - Wikipedia

Time to look into that too...

So, Epigram is dependently typed and has a 2-dimensional syntax! - Another reason why code editors need to evolve.

It appears that the most popular up-in-the-sky proof assistants that are often mentioned on LtU don't exploit the same kind of dependent typing as seen in Epigram (1 or 2). Looks like it's quite novel... cue Eric on type-systems of the future!

paks8150

Here is my take on the homework:

1. Without looking at the definitions from the standard prelude, define the following library functions using recursion.

- Decide if all logical values in a list are True:

and' :: [Bool] -> Bool
and' [] = True
and' (False:_)  = False
and' (_:xs)     = and xs

- Concatenate a list of lists:

concat' :: [[a]] -> [a]
concat' [] = []
concat' (xs:xss) = xs ++ concat' xss

- Produce a list with n identical elements:

replicate' :: Int -> a -> [a]
replicate' 0 x = []
replicate' (n+1) x = x:replicate' n x

- Select the nth element of a list

(!!@) :: [a] -> Int -> a
(!!@) (x:_) 0 = x
(!!@) (_:xs) (n+1) = xs !!@ n

- Decide if a value is an element of a list:

elem' :: (Eq a) => a -> [a] -> Bool
elem' _ [] = False
elem' x (y:ys) | x == y = True
               | otherwise = elem' x ys

2. Define a recursive function merge:: Ord a => [a] -> [a] -> [a] that merges two sorted lists to give a single sorted list.

merge:: (Ord a) => [a] -> [a] -> [a]
merge [] [] = []
merge xs [] = xs
merge [] ys = ys
merge (x:xs) (y:ys) | x < y = x:merge xs (y:ys)
                    | x == y = x:y:merge xs ys
                    | otherwise = y:merge (x:xs) ys

3. Define a recursive function msort :: Ord a => [a] -> [a] that implements merge sort

msort :: (Ord a) => [a] -> [a]
msort [] = []
msort [x] = [x]
msort xs = merge (msort ys) (msort zs)
           where [(ys,zs)] = halve xs

halve :: [a] -> [([a],[a])]
halve [] = []
halve xs = [(take n xs, drop n xs)]
           where n = (length xs `div` 2)

In reply to {0}

Download:[Pending]