Я пытаюсь разобрать строку с натуральными числами в Агде. например, результатstringListToℕ "1,2,3" должно бытьJust (1 ∷ 2 ∷ 3 ∷ [])

My current code is not quite right or by any means nice, but it works. However it returns the type: Maybe (List (Maybe ℕ))

Вопрос в том:

How to implement the function stringListToℕ in a nice way (compared to my code); it should have the type Maybe (List ℕ)

(optional, not important) How can I convert the type Maybe (List (Maybe ℕ)) to Maybe (List ℕ)?

Мой код:

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 >>= λ 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 -> 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"
-- => just (just 1 ∷ just 2 ∷ just 3 ∷ [])

EDIT

Я пытался написать функцию преобразования, используяfrom-just, но это дает ошибку при проверке типа:

  conv : Maybe (List (Maybe ℕ)) → Maybe (List ℕ) 
  conv (just xs) = map from-just xs
  conv _ = nothing

ошибка:

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