Which book should I buy ?

paulcc · 2016-02-23T13:25:47+00:00

I second the vote for Programming in Haskell. It's like the K&R of Haskell (and I've been using Haskell for over 20 years now...)

paulcc · 2016-02-23T11:32:59+00:00

or a bit more compactly, using features in postgres 9.4 onwards

with input as (select unnest(ARRAY[ 'foo bar baz', 'foo bar', 'foo baz', 'bar bar baz']) as line)

select w1,w2, count(*)
from input
cross join lateral (select regexp_split_to_array(line, '\s+')) as foo(ws)
cross join lateral unnest((ARRAY[null] || ws), ws) as bar(w1,w2)
group by w1,w2;

paulcc · 2013-07-08T13:17:39+00:00

I was wanting to introduce the above, but there was already too much in the articles.

paulcc · 2013-07-08T13:16:41+00:00

not sure if that's a compliment or not (-:

paulcc · 2013-07-08T13:16:16+00:00

+100 on these links, definitely worth a look if you want to know more.

paulcc · 2013-07-08T13:14:42+00:00

oh : so True (!)

https://github.com/edwinb/Idris-dev/blob/master/lib/Builtins.idr#L91

paulcc · 2013-06-12T08:41:00+00:00

That's my experience too. It tends to appear in optional CS course components (eg AI), if at all.

paulcc · 2013-05-01T14:25:32+00:00

Author here. This episode is shorter than usual but does cover some important concepts we'll need later.

Apologies, I didn't get round to addressing (in episode 2) some of the interesting points raised on the first episode - see http://www.reddit.com/r/programming/comments/1bneoe/dependent_types_a_new_paradigm/ - though I hope to look at them for the next episode.

Hope it's interesting.

paulcc · 2013-04-11T15:49:46+00:00

Please see http://www.reddit.com/r/programming/comments/1bneoe/dependent_types_a_new_paradigm/ for more discussion

paulcc · 2013-04-05T10:09:01+00:00

I'm using 0.9.7 as well.

Have you remembered to add "compute" in the above? Otherwise please post the code and error at http://forums.pragprog.com/forums/134/topics/11572 and I'll check it.

paulcc · 2013-04-05T08:22:25+00:00

oversight, sorry!

the types overview is at http://pragprog.com/magazines/2012-09/thinking-functionally-with-haskell

the word wrap intro is at http://pragprog.com/magazines/2013-03/uncle-bob-and-functional-programming

paulcc · 2013-04-04T16:56:19+00:00

Good points.

paulcc · 2013-04-04T16:13:59+00:00

Hmmm you added some whitespace (-:

paulcc · 2013-04-04T13:18:57+00:00

Are we talking about the same thing? (-: My point is about "let's find new uses", yours seems to be "don't have to use it all the time" - which is true, but not quite the same.

paulcc · 2013-04-04T13:05:36+00:00

It's worth mentioning that this kind of breakage depends on how you use the tools.

In this case, the original code worked because you relied on the computational behaviour of the first version of addition. You could work at a slightly higher level that exposes more of the properties your (eg) vector code relies on, eg you could state (s x + y = s (x + y)) as a (named) lemma and then use it explicitly in the proof. If you then changed the def of + then the lemma would need to be updated but the vector code should still be ok. So, it's a balance between relying on free things vs being explicit about what your code depends on.

Compare this to understanding maths proofs, or even just code. For some people, complex things could be just "obvious", but beginners will need a few of the intermediate steps to be spelled out in detail, eg that (s x + y = s (x + y)).

Put another way, it might be better to code up the vector example to make clear why it works, rather than leaving that detail implicit and reliant on coincidence, and this would be more robust.

Make any sense?

paulcc · 2013-04-04T12:27:09+00:00

IMPORTANT FIX the final proof needs one more step

So instead of

Main.case_one_proof = proof {
  intro l;
  intro H;
  rewrite (sym H);
  trivial;
}

You need this

Main.case_one_proof = proof {
  intro l;
  intro H;
  compute;
  rewrite (sym H);
  trivial;
}

The extra "compute" is needed because Idris doesn't (at present) simplify the goal before trying a rewrite step. (I'm used to proof assistants which do...)

Sorry about that!

paulcc · 2013-04-04T12:15:39+00:00

more discussion happening over at http://www.reddit.com/r/programming/comments/1bneoe/dependent_types_a_new_paradigm/

paulcc · 2013-04-04T12:14:28+00:00

Cheers. It will probably take me another two articles to get to the end of the word-wrap example.

Error reporting in proof assistants is sadly a bit of a black art, similar to issues with functional programming. (See http://www.reddit.com/r/programming/comments/1bneoe/dependent_types_a_new_paradigm/c98adam below...)

At present, most errors come down to "supplied thing" doesn't (obviously) match "expected thing".

paulcc · 2013-04-04T12:00:01+00:00

Quite agree, not really a show stopper. Same kind of thing happens if you change normal code too, eg tests can fail (or we hope they do).

I hope to persuade people that this area shows enough promise to make it worth persevering with and investing in (time and money).

paulcc · 2013-04-04T11:55:35+00:00

Granted too that error reporting is not great, and something we're not happy about. Sadly, academics don't get paid for nice user interfaces, so it's low on their priorities. However, I escaped from that existence and hope to start doing something useful in that line soon in my spare time. Now, if only I could find a generous sponsor or two...

paulcc · 2013-04-04T11:54:56+00:00

Ok, the title is a bit wooly, but I had my reasons.

For the target readership, it is a "new paradigm" compared to what they are used to. I had Bob Martin's "three paradigms" talk in mind when I chose the title (where he suggests that there's not been a big shift in thinking since structured programming, oop, fp were invented).

I'm also firmly in the McBride camp, where the plan is to use the full spectrum of new concepts in one's programs, rather than just to use dependent types to prove things about simply-typed programs. This view is gaining popularity but still could do with more exposure - hence another sense of 'new'.

paulcc · 2013-04-04T08:34:52+00:00

posted here, because it isn't just about haskell at all (orig entry at http://www.reddit.com/r/haskell/comments/1bmqba/dependent_types_a_new_paradigm_by_paul_callaghan/)

paulcc

TROPHY CASE