3 ms·

For those curious what Idris is, from http://www.idris-lang.org/ http://www.idris-lang.org/ : "Idris is a general purpose pure functional programming language w

by jcurbo 13y ago

For those curious what Idris is, from http://www.idris-lang.org/ 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 https://www.youtube.com/watch?v=vkIlW797JN8 David Christiansen at Haskell DC: http://bmsherman.github.io/idris-drc-3-26-14/ 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/ http://www.idris-lang.org/documentation/

14113 13y ago
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 http://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf
ryanartecona 13y ago
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 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/ 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!

by jcurbo 13y ago

14113 13y ago

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 http://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf

ryanartecona 13y ago

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 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/ 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!