Agda：用数字解析一个字符串

Question

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

我目前的代码不是很好，或者任何方式都不错，但它可以工作。 但是它返回类型： Maybe (List (Maybe ℕ))

的问题是：

1. 如何实现在一个不错的方式功能stringListToℕ（相对于我的代码）; 它应该有类型Maybe (List ℕ)

2. （可选，并不重要）我怎么能Maybe (List (Maybe ℕ))的类型转换为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 ∷ []) 

编辑

我试着写使用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 

Answer 1

我把重写你的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 

此外，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 

你可以找到Data.Listsequence;我们还必须指定我们想要使用哪个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 ℕ))成Maybe (List ℕ)，例如：

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

对，这并没有太大的作用。如果它们都是just，我们希望转换保留这些元素。 isNothing已经完成了这部分的检查，但它无法摆脱内层Maybe图层。

from-just可能工作，因为我们知道，当我们使用它时，List的所有元素都必须是just x一些x。问题是conv目前的形式是错误的 - from-just只能在Maybe值为just x时起作用Maybe A → A类型的功能！我们很可能会做这样的事情：

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

而且由于from-list表现为Maybe A → ⊤时给出nothing，我们esentially努力构建与类型都⊤和ℕ的元素异构名单。让我们放弃这个解决方案，我将展示一个更简单的方法（事实上，它应该类似于这个答案的第一部分）。

我们都给出了Maybe (List (Maybe ℕ))我们给两个目标：

• 采取内List (Maybe ℕ)（如果有的话），检查是否所有元素都是just x在这种情况下把他们都变成包裹在一个列表just，否则返回nothing

• 壁球双倍Maybe层成一个

好吧，第二点听起来很熟悉 - 这是monads可以做的事！我们得到：

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

此功能可以与任何单子的工作，但我们会没事的与Maybe。

而对于第一部分，我们需要一种方法来把一个List (Maybe ℕ)成Maybe (List ℕ) - 也就是说，我们要交换层而传播的可能误差（即nothing）到外层。 Haskell有专门的这种类型的类型（Traversable从Data.Traversable），this question有一些很好的答案，如果你想知道更多。基本上，这是关于在收集“副作用”的同时重建结构。如果版本仅适用于List s，我们会再次回到sequence。

目前仍然一件遗失了，让我们来看看我们到目前为止有：

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层内。这就是函子实例发挥作用的地方（你可以单独使用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 

Answer 2

我有一个尝试不去聪明，使用简单的递归函数而不是stdlib的魔法。 parse xs m ns通过记录已经在m中读取的（可能为空的）前缀来解析xs，同时保持已经在累加器ns中解析的数字列表。

如果发生解析失败（非识别字符，连续两次,等），所有内容都会丢失，我们将返回nothing。

module parseList where 

open import Data.Nat 
open import Data.List 
open import Data.Maybe 
open import Data.Char 
open import Data.String 

isDigit : Char → Maybe ℕ 
isDigit '0' = just 0 
isDigit '1' = just 1 
isDigit '2' = just 2 
isDigit '3' = just 3 
isDigit _ = nothing 

attach : Maybe ℕ → ℕ → ℕ 
attach nothing n = n 
attach (just m) n = 10 * m + n 

Quote : List Char → Maybe (List ℕ) 
Quote xs = parse xs nothing [] 
    where 
    parse : List Char → Maybe ℕ → List ℕ → Maybe (List ℕ) 
    parse []   nothing ns = just ns 
    parse []   (just n) ns = just (n ∷ ns) 
    parse (',' ∷ tl) (just n) ns = parse tl nothing (n ∷ ns) 
    parse (hd ∷ tl) m  ns with isDigit hd 
    ... | nothing = nothing 
    ... | just n = parse tl (just (attach m n)) ns 

stringListToℕ : String → Maybe (List ℕ) 
stringListToℕ xs with Quote (toList xs) 
... | nothing = nothing 
... | just ns = just (reverse ns) 

open import Relation.Binary.PropositionalEquality 

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

Answer 3

下面是从维图斯代码作为使用的阿格达前奏

module Parse where 

open import Prelude 

-- Install Prelude 
---- clone this git repo: 
---- https://github.com/fkettelhoit/agda-prelude 

-- Configure Prelude 
--- press Meta/Alt and the letter X together 
--- type "customize-group" (i.e. in the mini buffer) 
--- type "agda2" 
--- expand the Entry "Agda2 Include Dirs:" 
--- add the directory 



open import Data.Product using (uncurry′) 
open import Data.Maybe using() 
open import Data.List using (sequence) 

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 


charsToℕ : List Char → Maybe ℕ 
charsToℕ [] = nothing 
charsToℕ list = stringToℕ (fromList list) 

notComma : Char → Bool 
notComma c = not (c == ',') 

-- Finally: 

charListToℕ : List Char → Maybe (List ℕ) 
charListToℕ = Data.List.sequence Data.Maybe.monad ∘ map charsToℕ ∘ splitBy  notComma 

stringListToℕ : String → Maybe (List ℕ) 
stringListToℕ = charListToℕ ∘ toList 


-- Test 

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

test2 : stringListToℕ "12,33" ≡ just (12 ∷ 33 ∷ []) 
test2 = refl 

test3 : stringListToℕ ",,," ≡ nothing 
test3 = refl 

test4 : stringListToℕ "abc,def" ≡ nothing 
test4 = refl