4 ms·

> I should probably edit the tutorial to that effect. Yes please do. Idris is a lovely language for bringing dependent types closer to the realm of production

by bjz_ 13y ago

> I should probably edit the tutorial to that effect. Yes please do. Idris is a lovely language for bringing dependent types closer to the realm of production code, but giving people false hopes is a little cruel :)

tel 13y ago
Take a look at ATS then! My understanding from playing around with it is it is trying to be C with dependent types.
- thinkpad20 13y ago
  ATS looks fascinating in concept, but what code examples I've seen, the syntax is terrible and it's ridiculously verbose. I'm sure you could write absolutely bulletproof code in it, but the productivity hit would render it almost unusable for large-scale projects. I might be off here, of course... but one of the lovely things about Haskell is that despite its reputation as a difficult language, once certain key concepts are tackled, it's relatively easy to program rapidly and create real world products (with a considerably higher assurance of correctness than most languages provide). ATS seems complex to a level that nearly guarantees its usage won't extend much beyond academia.
  - bjz_ 13y ago
    Indeed. I love the idea of ATS, but it seems like it would be a challenge to wrangle with. Whilst Rust isn't a flexible and powerful as ATS, it seems to be much easier to handle at the moment.
    - doublec 13y ago
      I think any language you're not familiar can seem like that - especially if it uses unfamiliar sigils or syntax. I feel similar about Rust for example as I'm not as experienced with it. But with ATS I can put programs together pretty quickly - all because I've learnt it.
      - bjz_ 13y ago
        Thanks! Yeah, it's hard when you haven't used a language all that much to judge. I wish the sold themselves better though. The website is atrocious for folks wanting to get started with some code. :(
  - doublec 13y ago
    If you use the non-dependently typed parts of ATS it is no more verbose than most ML variants. If you use it without the GC then verbosity increased because you need to add calls to free memory. If you add proofs or dependent types then declaring those adds more. I've used it in moderately sized production programs and it's similar to using OCaml or other ML in terms of productivity. Once you're familiar with the language of course. If I paraphrase what you said about Haskell it's true for ATS too: "but one of the lovely things about ATS is that despite its reputation as a difficult language, once certain key concepts are tackled, it's relatively easy to program rapidly and create real world products (with a considerably higher assurance of correctness than most languages provide)." The key, like any language, is learning the concepts. I think people assume ATS is more difficult than it is is because much of the documentation and examples for it use a verbose style and heavy proofs. A post I wrote a while back attempts to gently introduce ATS dependent types and you can see that the non-dependently typed examples are very similar to any other ML language: http://bluishcoder.co.nz/2010/09/01/dependent-types-in-ats.html http://bluishcoder.co.nz/2010/09/01/dependent-types-in-ats.h...
    - tel 13y ago
      And to be clear, ridiculously verbose, dense, and unreadable proofs is the UX failing of most DT languages today. My understanding is that ATS is not significantly better or worse in that department.
    - bjz_ 13y ago
      > If you use it without the GC then verbosity increased because you need to add calls to free memory The issue is that is the default mode I would like to work in. Rust is designed to make that the natural mode of working, rather than the exception. Fast, deterministic operations should be easier and more succinct than the managed alternatives – in the context of a systems language that is. > people assume ATS is more difficult than it is is because much of the documentation and examples for it use a verbose style and heavy proofs. Then they need better docs. And a better website! And better marketing!
      - doublec 13y ago

by bjz_ 13y ago

tel 13y ago

Take a look at ATS then! My understanding from playing around with it is it is trying to be C with dependent types.

thinkpad20 13y ago
ATS looks fascinating in concept, but what code examples I've seen, the syntax is terrible and it's ridiculously verbose. I'm sure you could write absolutely bulletproof code in it, but the productivity hit would render it almost unusable for large-scale projects. I might be off here, of course... but one of the lovely things about Haskell is that despite its reputation as a difficult language, once certain key concepts are tackled, it's relatively easy to program rapidly and create real world products (with a considerably higher assurance of correctness than most languages provide). ATS seems complex to a level that nearly guarantees its usage won't extend much beyond academia.
- bjz_ 13y ago
  Indeed. I love the idea of ATS, but it seems like it would be a challenge to wrangle with. Whilst Rust isn't a flexible and powerful as ATS, it seems to be much easier to handle at the moment.
  - doublec 13y ago
    I think any language you're not familiar can seem like that - especially if it uses unfamiliar sigils or syntax. I feel similar about Rust for example as I'm not as experienced with it. But with ATS I can put programs together pretty quickly - all because I've learnt it.
    - bjz_ 13y ago
      Thanks! Yeah, it's hard when you haven't used a language all that much to judge. I wish the sold themselves better though. The website is atrocious for folks wanting to get started with some code. :(
- doublec 13y ago
  If you use the non-dependently typed parts of ATS it is no more verbose than most ML variants. If you use it without the GC then verbosity increased because you need to add calls to free memory. If you add proofs or dependent types then declaring those adds more. I've used it in moderately sized production programs and it's similar to using OCaml or other ML in terms of productivity. Once you're familiar with the language of course. If I paraphrase what you said about Haskell it's true for ATS too: "but one of the lovely things about ATS is that despite its reputation as a difficult language, once certain key concepts are tackled, it's relatively easy to program rapidly and create real world products (with a considerably higher assurance of correctness than most languages provide)." The key, like any language, is learning the concepts. I think people assume ATS is more difficult than it is is because much of the documentation and examples for it use a verbose style and heavy proofs. A post I wrote a while back attempts to gently introduce ATS dependent types and you can see that the non-dependently typed examples are very similar to any other ML language: http://bluishcoder.co.nz/2010/09/01/dependent-types-in-ats.html http://bluishcoder.co.nz/2010/09/01/dependent-types-in-ats.h...
  - tel 13y ago
    And to be clear, ridiculously verbose, dense, and unreadable proofs is the UX failing of most DT languages today. My understanding is that ATS is not significantly better or worse in that department.
  - bjz_ 13y ago
    > If you use it without the GC then verbosity increased because you need to add calls to free memory The issue is that is the default mode I would like to work in. Rust is designed to make that the natural mode of working, rather than the exception. Fast, deterministic operations should be easier and more succinct than the managed alternatives – in the context of a systems language that is. > people assume ATS is more difficult than it is is because much of the documentation and examples for it use a verbose style and heavy proofs. Then they need better docs. And a better website! And better marketing!
    - doublec 13y ago