[deltaonenine]

Basically the man wants two opposite things.

He wants contracts which is basically dependent types. These rules live in types and already exists in agda, Idris and coq and has a range of tradeoffs.

Essentially these languages can enforce static checks and "contracts" so powerful you don't need unit tests. These "contracts" cover more ground and are safer then tests. The tradeoff is you need a big brain and lots of time to write these things.

Then he wants a language that is truly dynamic. Which is like the opposite.

[zaphar]

Actually he wants 6 different things. Some of those six different things might live in the same language some of them wouldn't but wanting six different things is in no way problematic. Different tools/toys for different jobs/hobbies.

[deltaonenine]

No he wants two things. Those 6 different things have isomorphisms and can be reduced down to two things.

Think of it like 1*2 && 2. Both expressions are isomorphic. Dependent types literally encompasses everything he wants.

[zaphar]

He doesn't want the building blocks though. I could build those 6 things in any number of languages. What he want's are languages that explore making them ergonomic at the language level. That's like saying everything is doable in assembly. Which I mean sure, but that doesn't mean we don't want more ergonomic abstractions of those things.

[anon291]

> 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.

[AnthonBerg]

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.

[anon291]

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.

[deltaonenine]

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.

[deltaonenine]

>What he want's are languages that explore making them ergonomic at the language level.

This is exactly what dependently typed languages like coq and idris are attempting to do. What he wants ALREADY exists and these things are trying to fulfill EXACTLY his intent. I am not attempting to talk about some obscure isomorphism.

You also cannot build all 6 things in any number of languages unless you are using those languages to build new languages. These checks exist at the type level, not at runtime, but pre-compile time.

[zaphar]

I think what you are missing is that the author of the article does not consider the affordances of those languages as sufficient exploration of the space. Just because they can express these things and are meant to fulfill his intent doesn't mean they succeed in the ways he wants.

[Jtsummers]

Importantly, he doesn't want these conflicting things in one language.