Syntactic error when building

[fabriceleal]

When I build IdrisWeb by

idris --build idris_web.ipkg

I get a syntactic error

./IdrisWeb/DB/SQLite/SQLiteNew.idr:321:17: error: not
    a terminator, expected: (....)
reset = if_left then ResetFromEnd else Reset 

I also saw a lot of if_valid scattered through the same file. My idris version: 0.9.14.2-git:f50a883

[david-christiansen]

I believe this is from an older version of effects. It'll need porting to
the new one.

/David (from phone)

[jmitchell]

While reading the paper I also started wondering about if_valid.

Based on the changelog it was introduced in v0.9.10. Poked around a bit with git bisect and identified these two commits, the first where if_valid was moved to oldeffects and the second where oldeffects was removed entirely.

• idris-lang/Idris-dev@4ba5460
• idris-lang/Idris-dev@f9fe153

[SimonJF]

Yup, this is all done oldeffects, as described in the ICFP13 paper. There was a brief period between oldeffects and neweffects where if_valid was introduced.

What if_valid does was basically a more specific version of the new effects system -- instead of allowing the result of an effectual operation to determine the output effect, the output effect was a sum type, and if_valid differentiated between it. It turned out to be a bit messy (as you can see!), and this is when Edwin added Resource-Dependent Algebraic Effects, as you can see in the TFP'14 paper.

The initial draft didn't have if_valid -- instead, it handled things on the value level, not making underlying calls unless everything was OK. This was messy, hence the inspiration for neweffects.

(I know mine refers to RDAEs, which in that case referred to the old system, which is confusing. Sorry about that).

Essentially though, there's a huge amount of bitrot to fix here to get it working with neweffects, which I'll have to get round to at some point. @david-christiansen did some work a while ago on porting the SQLite library to neweffects though, which might be useful.

[ericqweinstein]

@david-christiansen & @SimonJF, this will be a bit longish, so! I'll preface by saying I'm very happy to make any PRs necessary to help get this project up & running with Idris 0.9.20 (I'm running 0.9.20.1).

The project now fails to build due to the recent FFI changes:

λ idris --install idris_web.ipkg
Entering directory `./src'
make: Nothing to be done for `all'.
Type checking ./IdrisWeb/Common/Random/RandC.idr
./IdrisWeb/Common/Random/RandC.idr:8:11:
When checking right hand side of getRandom with expected type
        IO Int

No such variable mkForeign

I think that this line (IdrisWeb/Common/Random/RandC.idr:8:11):

getRandom min max = mkForeign (FFun "random_number" [FInt, FInt] FInt) min max

should now be:

getRandom min max = foreign FFI_C "random_number" (Int -> Int -> IO Int) min max

Next, it looks like we need to update the package syntax:

λ idris --install idris_web.ipkg
Entering directory `./src'
make: Nothing to be done for `all'.
Type checking ./IdrisWeb/Common/Random/RandC.idr
Can't find import Effects

I think this change to idris_web.ipkg will do it:

package idrisweb

opts = "--typecase"
pkgs = effects, simpleparser

At this point, we start getting the above-noted if_* errors (IdrisWeb/DB/SQLite/SQLiteNew.idr:321:17):

reset = if_left then ResetFromEnd else Reset

I'm happy to make the FFI and package changes (in separate PRs) if the incremental improvement seems worthwhile; if you have the time to provide some guidance, I'm also happy to work on porting to the new Effects library or doing whatever needs doing.

Thanks so much for your work on this project! I've only just started working with Idris, but love it so far.

[david-christiansen]

I'd be happy to answer what questions I can if you want to work on de-bitrotting this lib. I haven't done the real work on this library, but I think you've identified what needs doing.

I don't think it's realistic to do these in separate PRs, because you can't test it until all of them are done. So I'd just update it to work with the newest Idris, and send a commit.

Thanks!

[ericqweinstein]

@david-christiansen Makes sense; I'll get cracking and submit a PR (though it may be large) when ready.

Are there preferred replacements for if_left and if_valid?

[david-christiansen]

On December 6, 2015 9:19:32 PM GMT+01:00, Eric Weinstein [email protected] wrote:

@david-christiansen Makes sense; I'll get cracking and submit a PR
(though it may be large) when ready.

Are there preferred replacements for if_left and if_valid?

---

Reply to this email directly or view it on GitHub:
#10 (comment)

Pattern matching on the result of the call does the same thing now!

[ericqweinstein]

👍

[ericqweinstein]

@david-christiansen Making good headway! Are these SQLite bindings relatively current (would they be useful in updating src/IdrisWeb/DB/SQLite/SQLiteNew.idr)?

[ericqweinstein]

Done so far:

• FFI updates (s/mkForeign/foreign/)
• Updated package syntax
• Replaced deprecated if_* with pattern matching

Working on:

• Updating SQLite bindings (it looks like the Effects library has moved ahead of this library)
• Parser updates
• CGI updates
• Any other Effects-related updates that need doing

[neduard]

@ericqweinstein Hey there, I was playing around with making IdrisWeb compile when I stumbled upon this issue and I see you already made some progress in solving it 👍
Any idea on when you might have time to complete the update? Or maybe share a "work-in-progress" branch on what you have updated so far?

[SimonJF]

Hi, sorry I seem to have missed this.

I'd say that this is in need of a rewrite now -- the Effects library that was current back when this library was written is deprecated now.

IdrisWeb provided:

• Effectful bindings for CGI, SQLite, and web sessions
• A web form DSL

What were you looking for from the library?

Reflecting on the web form DSL, I now think there are better ways of doing this (Formlets, in particular) and this implementation, while an interesting experiment, rather overcomplicates things.

[neduard]

@SimonJF oh I see, I wanted to setup a simple webpage using Idris. I want to learn the language and I thought working with already existing, simple code, would be a very good learning experience.

[ericqweinstein]

@neduard Thanks for reminding me about this! I sort of fell down a rabbit hole and agree with @SimonJF that this probably needs to be rewritten, given the changes in Idris and the Effects library since this repo was started. I'm happy to collaborate on that—things are a bit hectic on my end this week, but I'm free to help out starting next. 👍