有没有更好的方法在 Idris 中编写嵌套案例？答案

【问题标题】：Is there a better way to write nested cases in Idris?有没有更好的方法在 Idris 中编写嵌套案例？
【发布时间】：2021-08-06 09:07:03
【问题描述】：

这是一段来自 Edwin 书中的 Idris 代码：

data DataStore : Type where
  MkData : (size : Nat) ->
           (items : Vect size String) ->
           DataStore

proccessInput : DataStore -> String -> Maybe (String, DataStore)
proccessInput store@(MkData size items) input =
  case map trim $ span (/= ' ') input of
    ("add", item) => Just ("ID " ++ show size ++ "\n", MkData _ (item :: items))
    ("get", val) => case all isDigit (unpack val) of
      False => Just ("Invalid command\n", store)
      True => case integerToFin (cast val) size of
        Nothing => Just ("Out of range\n", store)
        (Just id) => Just (index id items ++ " \n", store)
    ("quit", "") => Nothing
    (_, _) => Just ("Invalid command\n", store)

我已经删除了一些我认为多余的代码（一些辅助函数），但我仍然发现代码有些多余。我觉得分案真的很丑。

【问题讨论】：

标签： functional-programming idris

【解决方案1】：

模式匹配绑定是处理可能失败的操作序列的方便表示法，这可能有助于减少嵌套案例块的某些最近性。

【讨论】：