title: Agda: parse a string with numbers
body: <p>I am trying to parse a string with natural numbers in Agda.
  e.g., the result of <code>stringListToℕ "1,2,3"</code> should be <code>Just (1 ∷ 2  ∷ 3 ∷ [])</code></p>
  
  <p>My current code is not quite right or by any means nice, but it works.
  However it returns the type:
      <code>Maybe (List (Maybe ℕ))</code></p>
  
  <p>The Question is:</p>
  
  <ol>
  <li><p>How to implement the function <code>stringListToℕ</code> in a nice way (compared to my code);
  it should have the type <code>Maybe (List ℕ)</code></p></li>
  <li><p>(optional, not important) How can I convert the type <code>Maybe (List (Maybe ℕ))</code> to <code>Maybe (List ℕ)</code>?</p></li>
  </ol>
  
  <p>My Code:</p>
  
  <pre><code>charToℕ : Char → Maybe ℕ
  charToℕ '0' = just 0
  charToℕ '1' = just 1
  charToℕ '2' = just 2
  charToℕ '3' = just 3
  charToℕ '4' = just 4
  charToℕ '5' = just 5
  charToℕ '6' = just 6
  charToℕ '7' = just 7
  charToℕ '8' = just 8
  charToℕ '9' = just 9
  charToℕ _   = nothing
  
  stringToℕ' : List Char → (acc : ℕ) → Maybe ℕ 
  stringToℕ' []       acc = just acc
  stringToℕ' (x ∷ xs) acc = charToℕ x &gt;&gt;= λ n → stringToℕ' xs ( 10 * acc + n )
  
  stringToℕ : String → Maybe ℕ
  stringToℕ s = stringToℕ' (toList s) 0 
  
  isComma : Char → Bool
  isComma h = h Ch.== ','
  
  notComma : Char → Bool
  notComma ',' = false
  notComma _ = true 
  
  {-# NO_TERMINATION_CHECK #-}
  split : List Char → List (List Char)
  split [] = []
  split s = l ∷ split (drop (length(l) + 1) s)
      where l : List Char
            l = takeWhile notComma s
  
  isNothing' : Maybe ℕ → Bool
  isNothing' nothing = true
  isNothing' _       = false
  
  isNothing : List (Maybe ℕ) → Bool 
  isNothing l = any isNothing' l
  
  -- wrong type, should be String -&gt; Maybe (List N)
  stringListToℕ : String → Maybe (List (Maybe ℕ))
  stringListToℕ s = if (isNothing res) then nothing else just res
                where res : List (Maybe ℕ)
                      res = map stringToℕ (map fromList( split (Data.String.toList s)))
  
  test1 = stringListToℕ "1,2,3"
  -- =&gt; just (just 1 ∷ just 2 ∷ just 3 ∷ [])
  </code></pre>
  
  <p><strong>EDIT</strong> </p>
  
  <p>I tried to write a conversion function using <code>from-just</code>, but this gives a error when type checking:</p>
  
  <pre><code>  conv : Maybe (List (Maybe ℕ)) → Maybe (List ℕ) 
    conv (just xs) = map from-just xs
    conv _ = nothing
  </code></pre>
  
  <p>the error is:</p>
  
  <pre><code>Cannot instantiate the metavariable _143 to solution
  (Data.Maybe.From-just (_145 xs) x) since it contains the variable x
  which is not in scope of the metavariable or irrelevant in the
  metavariable but relevant in the solution
  when checking that the expression from-just has type
  Maybe (_145 xs) → _143 xs
  </code></pre>