# Is it possible to reason about memory just by looking at type signatures?

If I have pure functional programming language with* very very smart optimization* proccess, is it possible to reason about memory usage, just by looking at type signature?

`add :: Int -> [Int] -> [Int]`

F. E. If the answer to my question would be yes, function add would allocate exactly (1+n+y)*sizeof(Int).

The reason I post the question here is, I struggle to find a counter example.

• What type system do you have in mind? Look into idris as an example of "smart" types (and you could even imagine some even more weird type system, with undecidable type inference in the general case, e.g. encode the memory usage or shape in the type) – Basile Starynkevitch Oct 6 '16 at 13:13
• How do you define "very very smart optimization"? As using a practically infinite ROM lookup table for every possible input? Because otherwise there are plenty of algorithms that need large temporary storage (consider scrypt and argon where this is the primary design goal) – CodesInChaos Oct 6 '16 at 13:13
• Contact also my friend Jérémie Salvucci. He is ending his PhD thesis on a subject quite similar to your question... – Basile Starynkevitch Oct 6 '16 at 13:16
• @CodesInChaos I think the algorithm you are talking about wouldn't be optimized, because it would be too expensive. Can you post a link to such an algorithm? – Ford O. Oct 6 '16 at 13:26
• Your function could simply ignore its first argument and generate all the permutations of the second one. That's `n!`. – gallais Oct 6 '16 at 13:30

No, the Halting Problem strikes again:

``````fn add(n: Int, ns: [Int]) -> [Int] {
loop {}
}
return ns.map(|v| {v+n})
}
``````

Depending on if `add` halts or not, it will allocate `O(length(ns))` memory or no memory.

Something to keep in mind is that the return type of a function does not guarantee the function will return something of that type.

A type signature provides the much weaker guarantee the function will not return something that is not of that type. In particular, it allows for returning nothing at all, as with an infinite loop or a power failure (though a power failure might not be considered pure) and out of band escapes, such as exceptions.

• The return type of a function does guarantee the function will return something of that type when working with total functional programming languages like Idris, where functions must terminate for all possible inputs. – Jack Oct 6 '16 at 18:06
• Turing-completeness is overrated. It's Tetris-completeness that's important. I used to think that you can't write operating systems, web servers, game loops, etc. in a total language, because total languages always halt and operating systems mustn't halt (an OS is an infinite loop, if it terminates, we call that "crashing" and get angry). But I since learned that an event loop (infinite recursion over data) can actually be modelled as finite co-recursion over co-data, thus making it total. – Jörg W Mittag Oct 6 '16 at 22:46
• @JörgWMittag What is the source of the "Tetris-completeness" phrase? Your comment is the only result for `"Tetris-completeness"` returned by Google. (You have recently used it in another comment.) – Dragomok Jun 18 '17 at 17:33
• @Dragomok: It was used by Edwin Brady, the designer of Iris, in a couple of talks. It is meant to highlight the difference between "can compute any computable function over the natural numbers" and "can be used write real-world programs", i.e. programs with state and I/O, which communicate with the OS, libraries, and the environment, interact with the user, and so on. Idris is a total pure functional language, so it is by definition not Turing-complete, and thus according to common myths cannot be used to write something like Tetris. But, there is an implementation of Asteroids in Idris. – Jörg W Mittag Jun 18 '17 at 19:57
• Which is another joke in itself, using Asteroids to prove Tetris-completeness is meant to mirror the way in which Turing-completeness is almost never demonstrated using Turing Machines, but rather λ-calculus, SKI Combinator Calculus, Cyclic Tag Systems, Game of Life, Rule 110, or Brainfuck. – Jörg W Mittag Jun 18 '17 at 19:59

No. Consider:

``````tailn :: Int -> [Int] -> [Int]
``````

which is the function that takes the nth tail of its second input (or error if this does not exist). This does not need to allocate any memory as the tails are all shared

You might be able to claim this for functions where there is only one possible implementation for the given signature (e.g. id), but then only if you also exclude pathological implementations (e.g. an implementation of id with a leak).

For a non pathological example of your original case that uses more memory:

``````flatReplicate :: int -> [Int] -> [Int]
flatReplicate n ns = concat (replicate n ns)
``````

which repeats its second argument n times and flattens this into a single list; this should be O(n^2) worst case.

• What about Pure functional language that doesn't share variables? – Ford O. Oct 6 '16 at 13:11
• Is it also possible to create function that uses more memory than type signature suggests? – Ford O. Oct 6 '16 at 13:17
• Its always possible to create a pathalogical implementation (language or function) that uses more memory pointlessly, but this probably isn't very interesting – jk. Oct 6 '16 at 13:41
• that is true, but then the compiler could optimize such a pointless allocation away! – Ford O. Oct 6 '16 at 15:17

It isn't even possible to tell what the function will do from that type signature, let alone how much memory it takes. Here are some possible valid implementations of that type signature:

``````add n ns = [0] -- memory O(1), time O(1)
add n ns = ns  -- memory O(length(ns)), time O(1)
add n ns = repeat n -- memory infinite, time infinite (assuming strictness)
``````

A less pathological example without infinite lists, and without simply ignoring (one of) the arguments:

``````add n ns = (take (n*n) \$ repeat n) ++ ns
-- memory O(n^2 + length(ns)), time … too tired to think about :-D
``````
• surely add n ns = ns is O(1) (additional) memory? if not how can it be O(1) time? or does you memory complexity include the input? – jk. Oct 6 '16 at 14:33