3 ms·

This is rather off-topic, but I want to learn Idris or any other purely functional programming language one day to the point where I would be able to read any p

This is rather off-topic, but I want to learn Idris or any other purely functional programming language one day to the point where I would be able to read any program, but most programs written in those languages are so terse and abstract, that I constantly find myself lost in them. The fact that most of those languages permit programmers to define custom operators doesn't help. I really wish someone would create something like https://cdecl.org/ https://cdecl.org/ but for programs in Haskell/Idris/etc. EDIT: On the article itself, I wonder how much time does it take to compile the resulting program?

akhilcacharya 8y ago
I'm in the same boat. I'd really love to see something that's a little bit more beginner friendly than Hoogle. It's honestly why I think avoiding operator overloading in Java/Go etc was a great idea.
- timjver 8y ago
  Isn't operator overloading something else than the ability to define custom operators?
  - btilly 8y ago
    What people do in practice with operator overloading is turn regular operators into custom operators that do something different. Your ability to customize behavior is not as extreme as being able to make any custom operators that you want. But the tradeoffs are definitely related.
    - seanmcdirmid 8y ago
      C# supports operator overloading but not custom operators. That means vectors get to use the plus operator for addition, but no Scalaesque ~~/ operators. C# is not a language that is generally criticized for operator soup like the ones that support custom operators.
      - ainar-g 8y ago
        Counter-examples: * C++ uses bitshift operators for IO. The (in?)famous std::cout << "hello world" << std::endl; Which is such an improvement over puts("hello world"); * Ruby on Rails components sometimes redefines `=` as a hash merge. E.g. this config.action_mailer.default_options = {from: 'no-reply@example.com'} actually adds `from` to the default options instead of overriding it completely.
      - btilly 8y ago
        C# may not be generally criticized for that. But there are certainly C# code bases that do get so criticized.
- jcelerier 8y ago
  strong disagree, looking up what an operator does takes 5 seconds of reading the doc - if it's a notation that you don't already know -, but the benefits when writing the code are immense.
clayrat 8y ago
I've updated the program to compile with the latest version of Idris (1.3): https://gist.github.com/clayrat/ad916323a4e672c1d7dfa3a0ecf18d85 https://gist.github.com/clayrat/ad916323a4e672c1d7dfa3a0ecf1... The compilation takes ~4 sec for me.
notthemessiah 8y ago
Idris is pretty well documented. It feels pretty inaccessible when you're just looking at the code, but in an editor with a plugin (Emacs, Atom, Vim), everything can be inspected, and it feels much more alive that way. Editing dependently-typed code has a particular development style which is very interactive, in which you fill in "holes" (code to be written) with help the from the editor/type-checker, providing feedback and suggestions. Resources: http://docs.idris-lang.org/en/latest/tutorial/index.html http://docs.idris-lang.org/en/latest/tutorial/index.html https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i... https://github.com/idris-hackers/software-foundations https://github.com/idris-hackers/software-foundations https://www.youtube.com/watch?v=4i7KrG1Afbk https://www.youtube.com/watch?v=4i7KrG1Afbk
- seanmcdirmid 8y ago
  The video is a useful start in understanding the Idris experience, but I guess it would be useful to see how much tooling helped in this definition of quick sort?
rtfeldman 8y ago
> I want to learn Idris or any other purely functional programming language one day to the point where I would be able to read any program, but most programs written in those languages are so terse and abstract, that I constantly find myself lost in them. Elm is purely functional and shares your design sensibilities on this. It is less terse (by design) than other purely functional languages and (as of the upcoming release) does not support user-defined operators. I know plenty of folks who got into Elm and then found Haskell and Idris much easier to approach, so it can unlock further learning too! https://guide.elm-lang.org https://guide.elm-lang.org
- seanmcdirmid 8y ago
  Does Elm support dependent types?
  - vimslayer 8y ago
    Definitely not, but the original commenter was looking for any purely functional programming language, not necessarily one with dependent types. I think we are years away from having an easily comprehensible and usable dependent type system, if it's even possible to have one.

akhilcacharya 8y ago

I'm in the same boat. I'd really love to see something that's a little bit more beginner friendly than Hoogle. It's honestly why I think avoiding operator overloading in Java/Go etc was a great idea.

timjver 8y ago
Isn't operator overloading something else than the ability to define custom operators?
- btilly 8y ago
  What people do in practice with operator overloading is turn regular operators into custom operators that do something different. Your ability to customize behavior is not as extreme as being able to make any custom operators that you want. But the tradeoffs are definitely related.
  - seanmcdirmid 8y ago
    C# supports operator overloading but not custom operators. That means vectors get to use the plus operator for addition, but no Scalaesque ~~/ operators. C# is not a language that is generally criticized for operator soup like the ones that support custom operators.
    - ainar-g 8y ago
      Counter-examples: * C++ uses bitshift operators for IO. The (in?)famous std::cout << "hello world" << std::endl; Which is such an improvement over puts("hello world"); * Ruby on Rails components sometimes redefines `=` as a hash merge. E.g. this config.action_mailer.default_options = {from: 'no-reply@example.com'} actually adds `from` to the default options instead of overriding it completely.
    - btilly 8y ago
      C# may not be generally criticized for that. But there are certainly C# code bases that do get so criticized.
jcelerier 8y ago
strong disagree, looking up what an operator does takes 5 seconds of reading the doc - if it's a notation that you don't already know -, but the benefits when writing the code are immense.

clayrat 8y ago

I've updated the program to compile with the latest version of Idris (1.3): https://gist.github.com/clayrat/ad916323a4e672c1d7dfa3a0ecf18d85 https://gist.github.com/clayrat/ad916323a4e672c1d7dfa3a0ecf1... The compilation takes ~4 sec for me.

notthemessiah 8y ago

Idris is pretty well documented. It feels pretty inaccessible when you're just looking at the code, but in an editor with a plugin (Emacs, Atom, Vim), everything can be inspected, and it feels much more alive that way. Editing dependently-typed code has a particular development style which is very interactive, in which you fill in "holes" (code to be written) with help the from the editor/type-checker, providing feedback and suggestions. Resources: http://docs.idris-lang.org/en/latest/tutorial/index.html http://docs.idris-lang.org/en/latest/tutorial/index.html https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i... https://github.com/idris-hackers/software-foundations https://github.com/idris-hackers/software-foundations https://www.youtube.com/watch?v=4i7KrG1Afbk https://www.youtube.com/watch?v=4i7KrG1Afbk

seanmcdirmid 8y ago
The video is a useful start in understanding the Idris experience, but I guess it would be useful to see how much tooling helped in this definition of quick sort?

rtfeldman 8y ago

> I want to learn Idris or any other purely functional programming language one day to the point where I would be able to read any program, but most programs written in those languages are so terse and abstract, that I constantly find myself lost in them. Elm is purely functional and shares your design sensibilities on this. It is less terse (by design) than other purely functional languages and (as of the upcoming release) does not support user-defined operators. I know plenty of folks who got into Elm and then found Haskell and Idris much easier to approach, so it can unlock further learning too! https://guide.elm-lang.org https://guide.elm-lang.org

seanmcdirmid 8y ago
Does Elm support dependent types?
- vimslayer 8y ago
  Definitely not, but the original commenter was looking for any purely functional programming language, not necessarily one with dependent types. I think we are years away from having an easily comprehensible and usable dependent type system, if it's even possible to have one.