6 ms·

> Certainly Haskell is said to have the most powerful type system going, Nah, Coq, Agda, Idris and any dependently typed language have Haskell beat -- their ty

by acomar 13y ago

> Certainly Haskell is said to have the most powerful type system going, Nah, Coq, Agda, Idris and any dependently typed language have Haskell beat -- their type systems are designed to be just as expressive as their value language. Haskell is certainly moving in this direction, especially with modern extensions. The issue is of course type inference breaks down in the face of these extensions, and Haskell is trying to maintain its powerful type inference as best it can. Certain combinations of extensions already force type annotations. > Still, I think core.typed does pretty damn well for being a standalone library. This is true, and I think the comparison to Haskell actually hurts the greater point you're trying to make. Haskell has full static types at its disposal, and comparing them to the optional typing of Clojure will always leave something wanting -- why draw that comparison when competing with Haskell is not the intention of the library?

chongli 13y ago
Nah, Coq, Agda, Idris and any dependently typed language have Haskell beat -- their type systems are designed to be just as expressive as their value language. That may be true, but it comes at a big cost: inference and decidability. Haskell's type system is designed to very carefully butt up against the limits of these features. Once you go full-spectrum dependent types, you lose all that.
- acomar 13y ago
  Agda and Coq retain inference and decidability by sacrificing Turing completeness. Terminating programs must terminate provably, and non-terminating programs must make concrete progress on every iteration. I'm not familiar enough with Idris to say how it tackles this issue - I do know that it is Turing complete. So with that said, you're absolutely right.
  - polymatter 13y ago
    Another language with a Turing complete type system is Shen [1] (previous life as Qi). Just wanted to put that out there as its a Lisp dialect that really pushes Lisp out there. [1] http://shenlanguage.org/ http://shenlanguage.org/
    - autodidakto 13y ago
      When it comes to awesomeness to fame ratio, I can't think of a language with a higher one than Shen. It's odd how little people talk about it. I, unfortunately, suspect it has to do with the people leading it.
      - tel 13y ago
        I've looked at Shen a few times and, honestly, I always get turned off by the syntax. There's not enough out there explaining why I should continue past that concern, and it seems to throw out what's nice about Lisp syntax in order to get halfway to Haskell's. I'm sure I'll take a look at it again sometime, but I'd really love some kind of intro that helped me to understand why it was worth the time investment to get to know it.
      - vdm 13y ago
        License has been a major turn off, just like Plan 9. Did they fix that yet?
  - nimble 13y ago
    > Agda and Coq retain inference and decidability by sacrificing Turing completeness. I don't know if I would phrase it that way, but there's a more important slight of hand going on here and I think chongli was right in spirit. Haskell takes care of (most) type level things for you with inference. Coq and Agda allow you to give very precise types to things, but those very precise types involve values that are not automatically inferred for you. It's certainly not the case that you can write the same annotation-free function in Coq that you would have written in Haskell and have a very precise type inferred for you.
adambard 13y ago
> Nah, Coq, Agda, Idris and any dependently typed language have Haskell beat I just knew someone was going to correct me on that statement, hence my "mainstream-ish" qualification. > why draw that comparison when competing with Haskell is not the intention of the library? I've got an unhealthy obsession with syntax, and I wanted to have a reference for people to see how things look in a "real" typed language. But, while I'm here, here's a bit I just wrote on /r/haskell (someone put this link there, but of course the haskellers were unimpressed) in defense of the library: --- Developing in Clojure tends to be a bit of an organic process, thanks to the deep REPL integration in many tools. You can evaluate arbitrary bits of your code as you go, swap things out, tweak whatever you like, and through a more-or-less exploratory process end up with a working bit of code. It's very freeing and very efficient, but if you've ever used a dynamic language for a large project, you know that this tends to create issues refactoring later unless every component is attached to a unit test. The power of core.typed is to let you, after the fact, lock down those function signatures and create what amounts to an automatic test suite.
- helloTree 13y ago
  This is the same for Haskell where it's also convenient to develop in the repl (ghci).
  - adambard 13y ago
    There's the repl, and then there's nREPL. I do like ghci, but I can't execute arbitrary chunks of Haskell directly from Vim.
    - freyrs3 13y ago
      This isn't a function of ghci or Haskell, that's an editor feature. If you want that kind of functionality than emacs is probably your best bet. Though you can send arbitrary code blocks from vim using vim-slime. [1] https://github.com/jpalardy/vim-slime https://github.com/jpalardy/vim-slime
      - 13y ago

by acomar 13y ago

chongli 13y ago

Nah, Coq, Agda, Idris and any dependently typed language have Haskell beat -- their type systems are designed to be just as expressive as their value language. That may be true, but it comes at a big cost: inference and decidability. Haskell's type system is designed to very carefully butt up against the limits of these features. Once you go full-spectrum dependent types, you lose all that.

acomar 13y ago
Agda and Coq retain inference and decidability by sacrificing Turing completeness. Terminating programs must terminate provably, and non-terminating programs must make concrete progress on every iteration. I'm not familiar enough with Idris to say how it tackles this issue - I do know that it is Turing complete. So with that said, you're absolutely right.
- polymatter 13y ago
  Another language with a Turing complete type system is Shen [1] (previous life as Qi). Just wanted to put that out there as its a Lisp dialect that really pushes Lisp out there. [1] http://shenlanguage.org/ http://shenlanguage.org/
  - autodidakto 13y ago
    When it comes to awesomeness to fame ratio, I can't think of a language with a higher one than Shen. It's odd how little people talk about it. I, unfortunately, suspect it has to do with the people leading it.
    - tel 13y ago
      I've looked at Shen a few times and, honestly, I always get turned off by the syntax. There's not enough out there explaining why I should continue past that concern, and it seems to throw out what's nice about Lisp syntax in order to get halfway to Haskell's. I'm sure I'll take a look at it again sometime, but I'd really love some kind of intro that helped me to understand why it was worth the time investment to get to know it.
    - vdm 13y ago
      License has been a major turn off, just like Plan 9. Did they fix that yet?
- nimble 13y ago
  > Agda and Coq retain inference and decidability by sacrificing Turing completeness. I don't know if I would phrase it that way, but there's a more important slight of hand going on here and I think chongli was right in spirit. Haskell takes care of (most) type level things for you with inference. Coq and Agda allow you to give very precise types to things, but those very precise types involve values that are not automatically inferred for you. It's certainly not the case that you can write the same annotation-free function in Coq that you would have written in Haskell and have a very precise type inferred for you.

adambard 13y ago

> Nah, Coq, Agda, Idris and any dependently typed language have Haskell beat I just knew someone was going to correct me on that statement, hence my "mainstream-ish" qualification. > why draw that comparison when competing with Haskell is not the intention of the library? I've got an unhealthy obsession with syntax, and I wanted to have a reference for people to see how things look in a "real" typed language. But, while I'm here, here's a bit I just wrote on /r/haskell (someone put this link there, but of course the haskellers were unimpressed) in defense of the library: --- Developing in Clojure tends to be a bit of an organic process, thanks to the deep REPL integration in many tools. You can evaluate arbitrary bits of your code as you go, swap things out, tweak whatever you like, and through a more-or-less exploratory process end up with a working bit of code. It's very freeing and very efficient, but if you've ever used a dynamic language for a large project, you know that this tends to create issues refactoring later unless every component is attached to a unit test. The power of core.typed is to let you, after the fact, lock down those function signatures and create what amounts to an automatic test suite.

helloTree 13y ago
This is the same for Haskell where it's also convenient to develop in the repl (ghci).
- adambard 13y ago
  There's the repl, and then there's nREPL. I do like ghci, but I can't execute arbitrary chunks of Haskell directly from Vim.
  - freyrs3 13y ago
    This isn't a function of ghci or Haskell, that's an editor feature. If you want that kind of functionality than emacs is probably your best bet. Though you can send arbitrary code blocks from vim using vim-slime. [1] https://github.com/jpalardy/vim-slime https://github.com/jpalardy/vim-slime
    - 13y ago