search

pigworker / CS410-17

being the lecture materials and exercises for the 2017/18 session of CS410 Advanced Functional Programming at the University of Strathclyde
263 stars 27 forks source link

Regarding Lecture 6 and the equation order problem with `findSplit`. #4

Open mbwgh opened 7 years ago

mbwgh commented 7 years ago

My github-fu isn't strong, so hopefully opening an issue as means of communication isn't in bad taste.

In lecture six (actually, at the end of lecture five, if you take the bite and try to implement it yourself), the last equation of findSplit makes you experience first-hand why the order of equations matters.

While following along with the lecture(s) I noticed that the last defining equation of _>[_]<_ gets highlighted in white for me. Since I had no idea what this meant (and after restarting the editor twice), I followed the instructions on the Agda Wiki on how to configure agda-mode highlighting, I saw that this particular color seems to be chosen for catchall-clauses, which - although I'm no expert - seems suspiciously related to me.

I use spacemacs in console-mode by the way, which because of the dark background makes this warning really stick out for me.

So it appears that Agda might be able to warn about these kind of issues, it might have actually been doing so in your case as well, but you didn't see it because of the peculiar choice of default colou for highlighting. I wonder if there is a -Wall kind of configuration to make these things more explicit with a textual message?

Anyway, thanks for making this course available online. Written tutorials don't capture what it means to "think like an Agdaist" in the same way.

mbwgh commented 7 years ago

Ok apparently this issue was discussed after all in Lecture 9 for the case of joinMaybe.