I am trying to parse a string with natural numbers in Agda.
e.g., the result of stringListToℕ "1,2,3"
should be 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 ℕ))
The Question is:
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 ℕ)
?
My 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 >>= λ 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
I tried to write a conversion function using from-just
, but this gives a error when type checking:
conv : Maybe (List (Maybe ℕ)) → Maybe (List ℕ)
conv (just xs) = map from-just xs
conv _ = nothing
the error is:
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
I took the liberty of rewriting your split
function into something more general which also works with the termination check:
open import Data.List
open import Data.Product
open import Function
splitBy : ∀ {a} {A : Set a} → (A → Bool) → List A → List (List A)
splitBy {A = A} p = uncurry′ _∷_ ∘ foldr step ([] , [])
where
step : A → List A × List (List A) → List A × List (List A)
step x (cur , acc) with p x
... | true = x ∷ cur , acc
... | false = [] , cur ∷ acc
Also, stringToℕ ""
should most likely be nothing
, unless you really want:
stringListToℕ "1,,2" ≡ just (1 ∷ 0 ∷ 2 ∷ [])
Let's rewrite it a bit (note that helper
is your original stringToℕ
function):
stringToℕ : List Char → Maybe ℕ
stringToℕ [] = nothing
stringToℕ list = helper list 0
where {- ... -}
And now we can put it all together. For simplicity I'm using List Char
everywhere, sprinkle with fromList
/toList
as necessary):
let x1 = s : List Char -- start
let x2 = splitBy notComma x1 : List (List Char) -- split at commas
let x3 = map stringToℕ x2 : List (Maybe ℕ) -- map our ℕ-conversion
let x4 = sequence x3 : Maybe (List ℕ) -- turn Maybe inside out
You can find sequence
in Data.List
; we also have to specify which monad instance we want to use. Data.Maybe
exports its monad instance under the name monad
. Final code:
open import Data.Char
open import Data.List
open import Data.Maybe
open import Data.Nat
open import Function
stringListToℕ : List Char → Maybe (List ℕ)
stringListToℕ = sequence Data.Maybe.monad ∘ map stringToℕ ∘ splitBy notComma
And a small test:
open import Relation.Binary.PropositionalEquality
test : stringListToℕ ('1' ∷ '2' ∷ ',' ∷ '3' ∷ []) ≡ just (12 ∷ 3 ∷ [])
test = refl
Considering your second question: there are many ways to turn a Maybe (List (Maybe ℕ))
into a Maybe (List ℕ)
, for example:
silly : Maybe (List (Maybe ℕ)) → Maybe (List ℕ)
silly _ = nothing
Right, this doesn't do much. We'd like the conversion to preserve the elements if they are all just
. isNothing
already does this part of checking but it cannot get rid of the inner Maybe
layer.
from-just
could work since we know that when we use it, all elements of the List
must be just x
for some x
. The problem is that conv
in its current form is just wrong - from-just
works as a function of type Maybe A → A
only when the Maybe
value is just x
! We could very well do something like this:
test₂ : Maybe (List ℕ)
test₂ = conv ∘ just $ nothing ∷ just 1 ∷ []
And since from-list
behaves as a Maybe A → ⊤
when given nothing
, we are esentially trying to construct a heterogeneous list with elements of type both ⊤
and ℕ
.
Let's scrap this solution, I'll show a much simpler one (in fact, it should resemble the first part of this answer).
We are given a Maybe (List (Maybe ℕ))
and we gave two goals:
take the inner List (Maybe ℕ)
(if any), check if all elements are just x
and in this case put them all into a list wrapped in a just
, otherwise return nothing
squash the doubled Maybe
layer into one
Well, the second point sounds familiar - that's something monads can do! We get:
join : {A : Set} → Maybe (Maybe A) → Maybe A
join mm = mm >>= λ x → x
where
open RawMonad Data.Maybe.monad
This function could work with any monad but we'll be fine with Maybe
.
And for the first part, we need a way to turn a List (Maybe ℕ)
into a Maybe (List ℕ)
- that is, we want to swap the layers while propagating the possible error (i.e. nothing
) into the outer layer. Haskell has specialized typeclass for this kind of stuff (Traversable
from Data.Traversable
), this question has some excellent answers if you'd like to know more. Basically, it's all about rebuilding the structure while collecting the "side effects". We'll be fine with the version that works just for List
s and we're back at sequence
again.
There's still one piece missing, let's look at what we have so far:
sequence-maybe : List (Maybe ℕ) → Maybe (List ℕ)
sequence-maybe = sequence Data.Maybe.monad
join : Maybe (Maybe (List ℕ)) → Maybe (List ℕ)
-- substituting A with List ℕ
We need to apply sequence-maybe
inside one Maybe
layer. That's where the Maybe
functor instance comes into play (you could do it with a monad instance alone, but it's more convenient). With this functor instance, we can lift an ordinary function of type a → b
into a function of type Maybe a → Maybe b
. And finally:
open import Category.Functor
open import Data.Maybe
final : Maybe (List (Maybe ℕ)) → Maybe (List ℕ)
final mlm = join (sequence-maybe <$> mlm)
where
open RawFunctor functor
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With