Hacker News new | past | comments | ask | show | jobs | submit login

You genuinely don't know how to write a TM that implements the identity function, or is there some technicality that it fails? If the latter, I'm not sure how it's relevant to my phrasing of the CTT.

>Types determine what computations make sense, even before any program is written at all.

>What category are you working on?

I have no idea what point you're trying to make with either of these comments.

>I'm not refuting the Church-Turing thesis! Why would I want to? I even believe it's true... in some models. ...

Regardless, my point is that the limitations you're bringing up seem to be very trivial and understate the extent to which it does apply. You're still wrong if you think the CTT is "true, but false if applied to matrix functions. No way could a computer handle that. They only know binaries numbers, not the matrix type. I mean, come on, I gave them a different name and everything!"




> You genuinely don't know how to write a TM that implements the identity function, or is there some technicality that it fails?

The inhabitants of the type `forall a. a -> a` (which, by the way, in an effectful, Turing-complete language, has more inhabitants than just the identity function) aren't in one-to-one correspondence with the inhabitants of the type `nat -> nat`. I asked for an isomorphism of types, you have to give me an isomorphism of types. Or maybe you don't know what “isomorphism” means in mathematics?

>> What category are you working on?

> I have no idea what point you're trying to make

Okay, you don't know what “isomorphism” means in mathematics.

> You're still wrong if you think the CTT is "true, but false if applied to matrix functions.

The CTT isn't “false if applied to matrix functions”. The CTT says nothing about functions at a type not isomorphic to `nat -> nat`. It would be like saying “SilasX is all wrong about frogs!”, when you never said anything about frogs (at least, in this discussion).

> No way could a computer handle that. They only know binaries numbers, not the matrix type. I mean, come on, I gave them a different name and everything!"

I write my programs in high-level programming languages, not machine language, though. The whole point to high-level programming languages is to reason in terms of their abstractions, not their possible implementations.




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: