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

> Types determine what the developer has certified as making sense.

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

> There can (and as far as we know, always does) exist an isomorphism between the higher-typed function that the developer has implemented and the TM-computable nat->nat.

Are you sure you're talking about isomorphisms in the mathematical sense? https://ncatlab.org/nlab/show/isomorphism I'm talking about a pair of morphisms:

    forward :: Foo -> Bar
    backward :: Bar -> Foo
Such that they compose to identities:

    backward . forward = id :: Foo -> Foo
    forward . backward = id :: Bar -> Bar
I'm pretty sure there's no isomorphism between `nat -> nat` and `forall a. a -> a`. Just to give one example.

> And and I was saying that the CTT is equivalent to saying that there is an isomorphism between a TM-computable nat->nat and any function that can be computed at all.

What category are you working on?

> you can't refute by CTT by defining Turing-complete language that lacks some critical access and say, "well, that's a function I guess it can't compute!"

I'm not refuting the Church-Turing thesis! Why would I want to? I even believe it's true... in some models. (Yes, truth is relative to models of a theory. Unlike provability.) I'm only saying that the CTT only claims what it claims. You're making extra conclusions that don't follow from the CTT's statement.




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: