Try Idris - Hackdot

Re:Try Idris by jcurbo on Sunday April 13, 2014 @01:41PM (#7582052)

For those curious what Idris is, from http://www.idris-lang.org/ : "Idris is a general purpose pure functional programming language with dependent types. Dependent types allow types to be predicated on values, meaning that some aspects of a program’s behaviour can be specified precisely in the type."

Here's a couple of talks about Idris:

Edwin Brady at London Haskell: https://www.youtube.com/watch?v=vkIlW797JN8

David Christiansen at Haskell DC: http://bmsherman.github.io/idris-drc-3-26-14/

And there's a tutorial and other docs available here: http://www.idris-lang.org/documentation/

[ Parent | on HN ]

Re:Try Idris by 14113 on Sunday April 13, 2014 @05:10PM (#7583041)

Just to note, Edwin was the original author of Idris, so I'd definitely recommend watching his talk.

Edit:

Given that my comment seems fairly high at the moment, I'll post a link to his PhD thesis, which seems to be the genesis of Idris for anyone interested: http://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf

[ Parent | on HN ]

Re:Try Idris by ryanartecona on Sunday April 13, 2014 @07:48PM (#7583713)

I'll add: if all this seems too opaque to jump into at once (and especially if you're unfamiliar with Haskell or other FP languages), don't give up on FP!

A "functional" language is not always a "pure" language, and a "pure functional" language certainly does not always have dependent types. These concepts build on each other.

A great intro to FP is "Programming in Standard ML". Concise, precise, and very approachable. SML is functional, but not pure nor dependently-typed (though purity is encouraged). http://www.cs.cmu.edu/~rwh/smlbook/book.pdf

Haskell is like SML with enforced purity, a different module/typeclass system, and default laziness. LYAH is the best intro. http://learnyouahaskell.com/

Idris is aimed primarily at those already familiar with Haskell, so don't be discouraged if the online REPL feels too foreign!

[ Parent | on HN ]