Hacker News new | ask | show | jobs
by anon291 1434 days ago
> That's like saying everything is doable in assembly

Dependent types are not doable in assembly though. Assembly has no notion of types. The claim that all languages are equivalent because they're turing complete has absolutely no relevance here. While true in terms of capability, the syntax and semantics of languages do make them different. One can add a contract library to idris. You cannot do that to assembly code because asembly code as a library. Such a thing is nonsensical since assembly's compilation model has no notion of type checking.
1 comments
AnthonBerg 1434 days ago
A dependently typed language is executed on a computer, therefore it is expressible in assembly code. Like sentences are expressed with words which are expressed with, say, letters. Letters are not sentences, but sentences do guide the expression of letters and vice versa. And sentences can indeed be made out of letters.
link
anon291 1433 days ago
Neural networks are expressed and represented by mathematical symbols, yet those mathematical symbols alone cannot make a prediction or do anything useful.

No one is saying assembly language cannot be used to write a dependently typed language system, with a type checker and runtime (which are one and the same in a DT language anyway). However, that does not make assembly language dependently typed.

You are committing the logical error of assuming that the result of a process means inputs to the process are equal to the outputs. Just because I could take grain and make it into bread doesn't mean grain is equivalent to bread.

link
deltaonenine 1434 days ago
When talking about these things there is a meta level we are targetting that you're not understanding. Types exist at a meta level and are part of the language.

Assembly language does not have types. What you can do is create a new language with assembly and have that language have types. The reason why it has to be done this way is because these types of checks CANNOT happen at runtime. It's a pre-runtime check that prevents the code from even running if it's not correct.

Think about it. Can you add types to assembly language without creating a new language? No.

link