Um, well the computation (can be set up to) proceeed(s) on algebraic datatypes, so this seems trivially easy.
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!" ?
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.
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.
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.
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.
> 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!