Introductory articles on Idris? (for general programmers)

[philip andrew]

Hi,

I came across this good article.

http://pragprog.com/magazines/2013-04/dependent-types

Are there any other articles for people who come from non-Haskell, non-mathematical background's such as myself where I come from a general programming background (but I have functional programming knowledge with Scala) ?

Thanks, Phil

[David Christiansen]

Hi Phil,

Have you seen the Idris tutorial in the documentation section of the web page?

Otherwise, I don't really know of anything.

/David

--
You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.
 
 

[philip andrew]

Yes I have, but its not simple, I mean its not like an "introduction to Java" with a Hello World etc.

Some of the concepts I don't understand yet, also its not saying, this is how you use a list, etc. I want a simple slow easy path into it and then to address these more interesting complex ideas slowly.

[David Christiansen]

2013/4/11 philip andrew <phili...@gmail.com>:

> Yes I have, but its not simple, I mean its not like an "introduction to
> Java" with a Hello World etc.
> Some of the concepts I don't understand yet, also its not saying, this is
> how you use a list, etc. I want a simple slow easy path into it and then to
> address these more interesting complex ideas slowly.

I see what you mean. I don't know of any other introductory material
like that - it might be a good idea to start with Learn You a Haskell,
which is close enough to Idris that the tutorial should begin to make
sense. Otherwise, I suppose you'll have to wait for more materials to
be produced!

/David

[Jesper Nordenberg]

On Thursday, April 11, 2013 6:42:08 AM UTC+2, philip andrew wrote:

I came across this good article.

http://pragprog.com/magazines/2013-04/dependent-types

Very helpful article, I hope they continue the series. I guess I'm in the same boat as you Philip, I have pretty solid knowledge about functional programming in Scala and Haskell, but dependently typed languages and proof assistants are totally new to me. I think you'll find more tutorial material on Coq than Idris currently.

/Jesper Nordenberg

[philip andrew]

Hi Jesper,

Yes I did the Scala course on Coursera, so I have a basic understanding of functional programming but come from an imperative background.

I wrote a small introduction article here http://www.philipandrew.com/practical-idris-programming-1/

Next I'd like to write a small one on lists, looking at the prelude list code.

Phil

[Paul Koerbitz]

Hi all,

for those who are looking for a good introduction on dependent types, I can also recommend 'software foundations' (http://www.cis.upenn.edu/~bcpierce/sf/). It uses Coq and not Idris, but from what I have seen it teaches the concepts fairly well and it should not be too hard to transfer them to Idris afterwards.

Paul

[Edwin Brady]

The tutorial as it stands is really just a crash course for people already familiar with functional programming in Haskell, since that was my initial target audience. But now that things are starting to work, it would be good to have an in-depth tutorial that doesn't make so many assumptions about the reader's background.

I'm not really sure of the best way of doing this though. It should probably be a collaborative effort. I have some idea about how such a thing might be structured, but haven't got around to starting.

By the way, you are all very welcome to extend the current tutorial if you see anything useful that could be added to it. More examples of the various concepts would help, in particular. If you do this, don't forget to add your name to the author list :).

Edwin.

[Paul Callaghan]

Hi

On Thursday, 11 April 2013 10:18:53 UTC+1, Jesper Nordenberg wrote:

Very helpful article, I hope they continue the series.

Cheers, there will be a few more, as time permits. I'm working on the next installment now. (Yes, being here is procrastination...) 

I'm grateful for any suggestions of what to cover in later articles!

Paul