7 ms·

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

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.

Jtsummers 4y ago
Importantly, he doesn't want these conflicting things in one language.
zaphar 4y ago
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 4y ago
  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 4y ago
    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 4y 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.
      - AnthonBerg 4y 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.
        deltaonenine 4y 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.
        anon291 4y 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.

Jtsummers 4y ago

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

zaphar 4y ago

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 4y ago
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 4y ago
  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 4y 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.
    - AnthonBerg 4y 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.
      - deltaonenine 4y 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.
      - anon291 4y 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.