idris-lang/Idris-dev — pull request #1651 by Melvar (2014-10-17 17:43:55+00:00)
Title: Turn pureM into a function

Logic:
```idris
pureM val = with_val val (pure ())
```
Let `val : a`, then
```idris
with_val val : Eff () xs (\v => xs' val) -> Eff a xs xs'
pure () : Eff () xs1 (\v => xs1 )
```
(after α-renaming in the type of `pure ()`). Now unify `xs` = `xs1` = `xs' val` to apply:
```idris
with_val val (pure ()) : Eff a (xs' val) xs'
```
Pulling `val` back out as an argument gives
```idris
pureM : (val : a) -> Eff a (xs' val) xs'
```

The following testcase from eff-tutorial §4.2 continues to work:
```idris
readInt : { [STATE (Vect n Int), STDIO] ==>
{ok} if ok then [STATE (Vect (S n) Int), STDIO]
else [STATE (Vect n Int), STDIO] }
Eff Bool
readInt = do let x = trim !getStr
case all isDigit (unpack x) of
False => pureM False
True => do putM (cast x :: !get)
pureM True
```