[pron]

:) You're just pushing the complexity into the validation of the algebraic type.

Look, a typed formalism does extra work of proving the type safety of the input. Checking a proof has a non-negligible complexity. If that cost could be ignored, then I have a computation model that solves NP problems in zero time: it has a type system that requires that the types form a proof certificate for the problem. All (obviously valid) inputs are then trivially reduced to "yes". In fact, you know very well that some type systems are Turing complete. If the complexity of validation is ignored, then those models can compute anything that's computable in zero time.

Types can prove things. The cost of the proof is well known, and is related to the difficulty of the problem. The universe doesn't let computational complexity slide. What, you think that God says, "oh, you clever boy, you chose a typed model so I'll let you have this proof for free!" ?

[tome]

> You're just pushing the complexity into the validation of the algebraic type.

Who says it needs to be validated, any more than your string needs to be validated?

> The universe doesn't let computational complexity slide. What, you think that God says, "oh, you clever boy, you chose a typed model so I'll let you have this proof for free!" ?

You're responding to something completely unrelated to my statement.

To be clear: I wasn't suggesting a typed lambda calculus.

[pron]

A tree is still more complex than strings, because it has rules: one parent per node and no cycles. Those need to be validated. But I have absolutely no problem accepting that it is possible to find an encoding of untyped LC which would bring it very close to a TM encoding. This wouldn't be surprising as LC doesn't do more computational work than TM at the validation step (unlike typed formalisms).

I specifically wrote that untyped LC is a borderline case, and it's unclear where precisely we want to draw the line. What is absoutely clear is that System F and TM are essentially, qualitatively and objectively very different, and when people try to compare them, they often, without noticing, describe two different computational problems, with two different complexities.

[l_dopa]

You're positing some new notion of complexity, without a definition, where lists are somehow fundamentally different than trees. Sorry, but that kind of claim requires more than just just an appeal to intuitions about how they might be implemented on a typical CPU. They're both just initial algebras.

The fact that your grand ideas about machine and language models doesn't apply to the lambda calculus should be a hint. We know how lambda calculus relates to typed languages: it's a degenerate case with a single type. Any differences in the complexity of type-inference or checking are between language models. You can't (without wildly waving your hands) formulate a meaningfully comparable problem for TM states.

[tome]

> A tree is still more complex than strings, because it has rules: one parent per node and no cycles. Those need to be validated.

Hmm, I'm not convinced that this is sufficient to show that strings are simpler.

After all, a string has rules too: a cell in the string is either at the beginning, or the end, or the middle, and it has neighbours left, right or not at all depending on those conditions, and at most one such neighbour in each direction. Even appeal to the physical world doesn't help. If I have a physical piece of DNA, how do I know it hasn't mutated so that two different strands branch off it and it becomes, essentially, a degenerate tree?

I do think that the thrust of your argument is correct but it's not as clear cut (at least not yet) as you seem to be making out.

> What is absoutely clear is that System F and TM are essentially, qualitatively and objectively very different

Absolutely agreed! If they weren't, I'd be happy writing my day-to-day code in Turing Machines.

[pron]

You're talking about the graphical representation of a string. A string is any stream of measurements (over time, if you like).

> If they weren't, I'd be happy writing my day-to-day code in Turing Machines.

And if they weren't, we'd see neurons or DNA using type-theory!

[tome]

Since you seem to have thought about the fine details of this much more than you are letting on here and on your blog post I suggest you post an addendum (or even a new blog post) to be more precise about what exactly they are. There's a lot missing as it stands, and interested readers like myself are left to fill in the blanks.