3 ms·

Yeah, the current problem is that Idris code is far less efficient than Rust code, because Idris boxes everything and erases all types, and also Idris's support

by devit 5y ago

Yeah, the current problem is that Idris code is far less efficient than Rust code, because Idris boxes everything and erases all types, and also Idris's support for borrowing seems less powerful than Rust (it lacks first-class mutable borrows as far as I can tell). It seems that fixing this is a research problem, which would lead to the holy grail of programming languages, i.e. an ultimate language that is as expressive as Idris and as efficient as Rust, and is thus essentially perfect.

siknad 5y ago
> an ultimate language that is as expressive as Idris and as efficient as Rust, and is thus essentially perfect. Are both Idris's expressiveness and Rust's efficiency (given stronger guarantees) perfect? Aren't theese languages really complex both to learn and to write? There are poblems without a solution, perfect and unique to all of them.
dwohnitmok 5y ago
> Idris's support for borrowing seems less powerful than Rust (it lacks first-class mutable borrows as far as I can tell). Depends on what you mean. Idris's notion of multiplicities essentially subsumes Rust's borrowing (there's some differences with affine vs linear types), so I can't think off the top of my head of things that you can ensure with Rust that you can't with Idris, but Rust has a lot more quality of life improvements that make things less clunky (also having a GC, Idris can get away with a lot less need for borrowing in the first place).
preseinger 5y ago
Expressiveness is not an unambiguous net good -- more expressiveness is not a priori better. Expressiveness carries costs of comprehension and coherence that need to be appropriately weighed in the contexts where the language will be applied. Programming languages are not theoretical things. They're concrete, practical tools that _enable_ other stuff. Engineering, not science.
- ImprobableTruth 5y ago
  How would you define expressiveness (as its commonly used, so a definition where Turing complete languages can have different expressiveness) if not as how much something can be simplified and thus aiding comprehension, rather than detracting from it? >Programming languages are not theoretical things. They're concrete, practical tools that _enable_ other stuff. Engineering, not science. You can't escape theory, engineering is applied science.
  - preseinger 5y ago
    Increasing expressiveness of a language necessarily increases its complexity. Comprehension is important but it's a function of "the whole stack" -- language and program both. > engineering is applied science. Absolutely. But the metrics are different.
  - matt_kantor 5y ago
    I'm not the person you replied to, but here's an analogy: it's easier to learn how to drive a car with an automatic transmission than a manual one, even though the latter is "more expressive".
    - ImprobableTruth 5y ago
      Heh, I would actually consider automatic transmission to be the more expressive one, since to me expressive means how easy it is to express something. Analogously e.g. C++ (manual) is more efficient and allows finer control, but makes it harder to express the same thing as in a 'higher level' (automatic) language. Otherwise, since Assembly provides the most control out of all, would you consider it the most expressive? ;-)
      - matt_kantor 5y ago
        I guess in my head "expressiveness" is some fuzzy combination of what you are able to do plus how easy it is to do those things. I'd consider a calculator that supports real numbers to be more expressive than one which only supports integers, all else being equal. Maybe this definition is idiosyncratic, though. It's certainly not objective.
zozbot234 5y ago
The Prusti effort to endow Rust with proof-carrying code is also worth mentioning. There are some reasons to expect this approach to be more fruitful than an actual extension of dependently-typed languages, since the type system features of Rust itself are hard to integrate with dependent types. (At best, it might be somewhat feasible to use the latter in the `const`, compile-time evaluated subset of the language.)

by devit 5y ago

siknad 5y ago

> an ultimate language that is as expressive as Idris and as efficient as Rust, and is thus essentially perfect. Are both Idris's expressiveness and Rust's efficiency (given stronger guarantees) perfect? Aren't theese languages really complex both to learn and to write? There are poblems without a solution, perfect and unique to all of them.

dwohnitmok 5y ago

> Idris's support for borrowing seems less powerful than Rust (it lacks first-class mutable borrows as far as I can tell). Depends on what you mean. Idris's notion of multiplicities essentially subsumes Rust's borrowing (there's some differences with affine vs linear types), so I can't think off the top of my head of things that you can ensure with Rust that you can't with Idris, but Rust has a lot more quality of life improvements that make things less clunky (also having a GC, Idris can get away with a lot less need for borrowing in the first place).

preseinger 5y ago

Expressiveness is not an unambiguous net good -- more expressiveness is not a priori better. Expressiveness carries costs of comprehension and coherence that need to be appropriately weighed in the contexts where the language will be applied. Programming languages are not theoretical things. They're concrete, practical tools that _enable_ other stuff. Engineering, not science.

ImprobableTruth 5y ago
How would you define expressiveness (as its commonly used, so a definition where Turing complete languages can have different expressiveness) if not as how much something can be simplified and thus aiding comprehension, rather than detracting from it? >Programming languages are not theoretical things. They're concrete, practical tools that _enable_ other stuff. Engineering, not science. You can't escape theory, engineering is applied science.
- preseinger 5y ago
  Increasing expressiveness of a language necessarily increases its complexity. Comprehension is important but it's a function of "the whole stack" -- language and program both. > engineering is applied science. Absolutely. But the metrics are different.
- matt_kantor 5y ago
  I'm not the person you replied to, but here's an analogy: it's easier to learn how to drive a car with an automatic transmission than a manual one, even though the latter is "more expressive".
  - ImprobableTruth 5y ago
    Heh, I would actually consider automatic transmission to be the more expressive one, since to me expressive means how easy it is to express something. Analogously e.g. C++ (manual) is more efficient and allows finer control, but makes it harder to express the same thing as in a 'higher level' (automatic) language. Otherwise, since Assembly provides the most control out of all, would you consider it the most expressive? ;-)
    - matt_kantor 5y ago
      I guess in my head "expressiveness" is some fuzzy combination of what you are able to do plus how easy it is to do those things. I'd consider a calculator that supports real numbers to be more expressive than one which only supports integers, all else being equal. Maybe this definition is idiosyncratic, though. It's certainly not objective.

zozbot234 5y ago

The Prusti effort to endow Rust with proof-carrying code is also worth mentioning. There are some reasons to expect this approach to be more fruitful than an actual extension of dependently-typed languages, since the type system features of Rust itself are hard to integrate with dependent types. (At best, it might be somewhat feasible to use the latter in the `const`, compile-time evaluated subset of the language.)