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

你可以找到sequence的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

考虑你的第二个问题:有很多方法可以将a Maybe (List (Maybe ?))变为a Maybe (List ?),例如:

silly : Maybe (List (Maybe ?)) ? Maybe (List ?)
silly _ = nothing

对,这没什么用.我们希望转换为保留元素,如果它们都是just.isNothing已经做了这部分检查,但它无法摆脱内层Maybe.

from-just 可以工作,因为我们知道,当我们使用它,的所有元素List必须是just x对于一些x.问题是,conv它目前的形式是错误的 - 只有当值为时才from-just作为类型的函数!我们可以做这样的事情:Maybe A ? AMaybejust x

test? : Maybe (List ?)
test? = conv ? just $ nothing ? just 1 ? []

并且由于from-list表现为Maybe A ? ?给定的时间nothing,我们正在尝试构建具有类型?和的元素的异构列表?.

让我们废弃这个解决方案,我会展示一个更简单的解决方案(事实上,它应该类似于这个答案的第一部分).

我们得到了一个Maybe (List (Maybe ?)),我们给了两个目标:

• 取内部List (Maybe ?)(如果有的话),检查是否所有元素都是,just x并且在这种情况下将它们全部放入包含在a中的列表中just,否则返回nothing

• 将双层Maybe压缩成一层

好吧,第二点听起来很熟悉 - 这是monad可以做的!我们得到:

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

这个功能可以适用于任何单子,但我们会很好Maybe.

对于第一部分,我们需要一种方法将a List (Maybe ?)变成a Maybe (List ?)- 也就是说,我们想要在将可能的错误(即nothing)传播到外层时交换层.Haskell有这种东西专门的类型类(Traversable来自Data.Traversable),如果你想了解更多,这个问题有一些很好的答案.基本上,所有这些都是在收集"副作用"的同时重建结构.对于仅适用于Lists 的版本我们会很好,我们又回来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一层内部应用.这就是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