Agda：用数字解析字符串

我正在尝试用 Agda 中的自然数解析字符串。 例如，结果stringListToℕ "1,2,3"应该Just (1 ∷ 2 ∷ 3 ∷ [])

我当前的代码不太正确，或者无论如何都不太好，但它可以工作。 但是它返回类型：Maybe (List (Maybe ℕ))

问题是：

1. 功能如何实现stringListToℕ以一种很好的方式（与我的代码相比）； 它应该有类型Maybe (List ℕ)

2. （可选，不重要）如何转换类型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

我尝试使用编写一个转换函数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

我冒昧地重写了你的split函数变成更通用的东西，也适用于终止检查：

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ℕ ""最有可能的是nothing，除非你真的想要：

stringListToℕ "1,,2" ≡ just (1 ∷ 0 ∷ 2 ∷ []) 

让我们重写一下（注意helper是你原来的stringToℕ功能）：

stringToℕ : List Char → Maybe ℕ
stringToℕ []   = nothing
stringToℕ list = helper list 0
  where {- ... -}

现在我们可以把它们放在一起。为了简单起见，我使用List Char到处撒上fromList/toList有必要的）：

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

你可以找到sequence in Data.List;我们还必须指定要使用哪个 monad 实例。Data.Maybe以名称导出其 monad 实例monad。最终代码：

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

还有一个小测试：

open import Relation.Binary.PropositionalEquality

test : stringListToℕ ('1' ∷ '2' ∷ ',' ∷ '3' ∷ []) ≡ just (12 ∷ 3 ∷ [])
test = refl

考虑你的第二个问题：有很多方法可以改变Maybe (List (Maybe ℕ)) into a Maybe (List ℕ)， 例如：

silly : Maybe (List (Maybe ℕ)) → Maybe (List ℕ)
silly _ = nothing

是的，这并没有多大作用。我们希望转换能够保留元素（如果它们全部）just. isNothing已经做了这部分检查，但它无法摆脱内部Maybe layer.

from-just could之所以有效，是因为我们知道当我们使用它时，List必须是just x对于一些x。问题是conv目前的形式是错误的 -from-just作为类型的函数Maybe A → A仅当Maybe值为just x！我们很可以做这样的事情：

test₂ : Maybe (List ℕ)
test₂ = conv ∘ just $ nothing ∷ just 1 ∷ []

自从from-list表现为Maybe A → ⊤当给予nothing，我们本质上是试图构建一个异构列表，其元素类型均为⊤ and ℕ.

让我们放弃这个解决方案，我将展示一个更简单的解决方案（事实上，它应该类似于这个答案的第一部分）。

我们被赋予了一个Maybe (List (Maybe ℕ))我们给出了两个目标：

• 采取内在的List (Maybe ℕ)（如果有），检查所有元素是否just x在这种情况下，将它们全部放入一个包含在just，否则返回nothing

• 压扁两倍Maybe层层合而为一

嗯，第二点听起来很熟悉——这是 monad 可以做的事情！我们得到：

join : {A : Set} → Maybe (Maybe A) → Maybe A
join mm = mm >>= λ x → x
  where
    open RawMonad Data.Maybe.monad

这个函数可以与任何 monad 一起使用，但我们可以使用Maybe.

对于第一部分，我们需要一种方法来转变List (Maybe ℕ) into a Maybe (List ℕ)- 也就是说，我们希望在传播可能的错误时交换层（即nothing）进入外层。 Haskell 有专门的类型类来处理这类东西（Traversable from Data.Traversable), 这个问题如果您想了解更多信息，有一些很好的答案。基本上，这都是关于重建结构，同时收集“副作用”。我们会选择适合的版本Lists，我们回到了sequence again.

还缺少一块，让我们看看到目前为止我们已经有了什么：

sequence-maybe : List (Maybe ℕ) → Maybe (List ℕ)
sequence-maybe = sequence Data.Maybe.monad

join : Maybe (Maybe (List ℕ)) → Maybe (List ℕ)
  -- substituting A with List ℕ

我们需要申请sequence-maybe里面一Maybe层。那就是Maybefunctor 实例开始发挥作用（您可以单独使用 monad 实例来完成，但它更方便）。通过这个函子实例，我们可以提升类型的普通函数a → b转化为类型的函数Maybe a → Maybe b。最后：

open import Category.Functor
open import Data.Maybe

final : Maybe (List (Maybe ℕ)) → Maybe (List ℕ)
final mlm = join (sequence-maybe <$> mlm)
  where
    open RawFunctor functor