- learn a new programming language
- contribute to an open-source project (the Idris source is on github )
- improve my Haskell programming skills (Idris is written in Haskell)
- learn more type theory
cabal install idris
Note: You’ll need to install the Haskell Platform (which includes cabal) beforehand.
So, time to start Idris! (types idris at the shell prompt…)
Nice ASCII art – reminds me of the good old 8-bit computer days. Version is 0.99...what does that mean? Is my version an almost perfect 1.0? So I head over to idris-lang.org and after only a few seconds I find what I need at this page.
Great – 0.99 is the alpha release of 1.0. Large parts of the language are now considered stable. There is also a book authored by Edwin Brady due to be published in March 2017. Seems like a good time to jump on board. I especially like this bit on the towards-version-1-0 page …
“Idris remains primarily a research tool, with the goals of exploring the possibilities of software development with dependent types, and particularly aiming to make theorem proving and verification techniques accessible to software developers in general”
This is what I like about Haskell – computer science theory made accessible, understandable and (possibly) usable in production code.
I find it amusing that there is ‘ABSOLUTELY NO WARRANTY’ but you can still type ‘:warranty.’ to obtain more details about the non-existence of the non-existent warranty. Now I’m forced to actually type ‘:warranty’ to see what happens or I won’t be able to sleep – ok, it spells out fully what the non-existence means legally so as to protect the copyright holders. Fair enough. Now I’ll check out the help…
:?
Good – only about a page. Nothing worse than getting a command listing 5 pages long that gives little clue as to what is important and what is not. And it appears that a few of the commonly used commands are the same as in Haskell.
The first command is :t to check the type of an expression. I’ll type this with no argument to see how Idris handles something stupid.
Now this is nice. It knows I’ve stuffed up and it tries to help. Compare this with Haskell (ghci) and we get
Now, I know nobody would do a mistake like this but what I like is that the Idris error message shows that the developers are trying hard to be kind. I’ll now play with :t a bit …
Responses are mostly as expected. I’m not sure what the type (2=2) actually means at the moment but Idris seems to be happy to accept it as a Type. Now I’ll do a :browse Prelude and then hit the TAB key to see what’s available.
It is interesting to see what category theoretic constructions are available – algebra, applicative, functor, and monad as well as the usual foldable and traversable. There are a couple of curious items too such as WellFounded and Uninhabited. And what is that JSNull – something to do with Javascript?!
Back to the command listing and there are some items just waiting to be explored…
Really interesting - especially for a mathematician. Now, it appears that to make further progress there are two ways to continue
1) Look at the exciting stuff first – do some simple proofs and see what all this dependent typing is all about.
2) Be patient, learn the basics of Idris first and then be able to do proofs without stumbling over gaps in background knowledge.
I’m choosing option 2 to get a firm foundation since I assume that just treating Idris as Haskell++ is not an efficient way to proceed.
In part 2 of this series I’ll dive into the basics using https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf and other materials from Edwin Brady’s blog at https://edwinb.wordpress.com/category/idris/ .
No comments:
Post a Comment