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